外延性の公理

(２つの集合が等しいことの定義)

先ず以下の記述があります。

theorem
 (for x holds x in X iff x in Y) implies X = Y;

記号論理で書けば

$$((\forall x )(x \in X \Leftrightarrow x \in Y) ) \Rightarrow X = Y$$

です。

これは,外延性の公理として知られるものです。
任意の$x$に対して,

$$x \in X \Leftrightarrow x \in Y$$

であるならば,２つの集合$X,Y$は等しい($X=Y$である) ことを主張しています。