$scheme\ SetEq$

以下は,

$$(\forall X1,X2 : (\forall x)(x \in X1 \Leftrightarrow P[x... ... \ (\forall x)(x \in X2 \Leftrightarrow P[x])) (X1 = X2 )$$

を表す公理図式です。

scheme SetEq { P[set] } :
  for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2
proof let X1,X2 be set such that
  A1: for x being set holds x in X1 iff P[x] and
  A2: for x being set holds x in X2 iff P[x];
  thus thesis from Extensionality(A1,A2);
end;

証明は,

$$A1: (\forall x)(x \in X1 \Leftrightarrow P[x])$$

$$A2: (\forall x)(x \in X2 \Leftrightarrow P[x])$$

を仮定すれば,関係式$A1, A2$に公理図式 $Extensionality(A1,A2)$が適用できることによって示されます。