Exercise 6, § 1

This solution was written by nemotron-3-ultra-free and judged by a machine. It is not Bourbaki's and it has not been checked by a person.

Let $\mathscr{T}$ be an equalitarian theory containing the sign $\in$ and the axiom A1': $(\forall y)(y = \tau_x((\forall z)(z \in x \Leftrightarrow z \in y)))$. We prove that the axiom of extent A1: $(\forall x)(\forall y)((x \subset y \text{ and } y \subset x) \Rightarrow (x = y))$ is a theorem in $\mathscr{T}$.

Let $x$ and $y$ be terms. Assume $x \subset y$ and $y \subset x$. By Definition 1 (tag 03H5), $x \subset y$ means $(\forall z)(z \in x \Rightarrow z \in y)$ and $y \subset x$ means $(\forall z)(z \in y \Rightarrow z \in x)$. Hence we have

Applying A1' to $x$ and $y$ (and renaming the bound variable $x$ to $u$ to avoid confusion) we obtain

We now show that the two relations $(\forall z)(z \in u \Leftrightarrow z \in x)$ and $(\forall z)(z \in u \Leftrightarrow z \in y)$ are equivalent for every $u$. Let $u$ be an arbitrary term. From (1), for any $z$ we have $z \in x \Leftrightarrow z \in y$. If $(\forall z)(z \in u \Leftrightarrow z \in x)$, then for any $z$, $z \in u \Leftrightarrow z \in x \Leftrightarrow z \in y$, so $(\forall z)(z \in u \Leftrightarrow z \in y)$. The converse implication is identical. Thus

By scheme S7 of Chapter I (which states that $(\forall u)(R \Leftrightarrow S) \Rightarrow (\tau_u R = \tau_u S)$), (3) yields

Combining (2) and (4) with the transitivity of equality (valid in any equalitarian theory) we conclude $x = y$.

Thus, under the hypothesis $x \subset y$ and $y \subset x$ we have proved $x = y$. Therefore A1 is a theorem in $\mathscr{T}$.