Exercise 2, § 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.

By Theorem 1 of § 1, the relation $(\forall x)(x \notin \emptyset)$ is a theorem; in particular, for any term $x$ we have $x \notin \emptyset$. Also by Theorem 1, the relation $\emptyset \subset X$ is a theorem for every set $X$; hence $\emptyset \subset \{x\}$ is a theorem.

By Definition 2 of § 1, the relation $z \in \{x\}$ is equivalent to $z = x$. Since equality is reflexive, $x = x$ holds, and therefore $x \in \{x\}$.

Now assume that $\emptyset = \{x\}$ were a theorem. Because $\emptyset \subset \emptyset$ is a theorem by Proposition 1 of § 1, we may substitute $\emptyset$ by $\{x\}$ in this relation to obtain $\{x\} \subset \emptyset$. The definition of inclusion (Definition 1 of § 1) gives $(\forall z)(z \in \{x\} \Rightarrow z \in \emptyset)$. Applying this to $z = x$ yields $x \in \{x\} \Rightarrow x \in \emptyset$. Since $x \in \{x\}$ is true, we would have $x \in \emptyset$, contradicting $x \notin \emptyset$ from Theorem 1. Therefore $\lnot(\emptyset = \{x\})$ is a theorem, i.e., $\emptyset \neq \{x\}$ is a theorem.

Since $\emptyset \neq \{x\}$ is a theorem (with $x$ free), we may instantiate $x$ with the term $\emptyset$. The existence of $\{\emptyset\}$ is guaranteed by Axiom A2 of § 1, which asserts $(\forall x)(\forall y)\operatorname{Coll}_z(z = x \text{ or } z = y)$; taking $x = y = \emptyset$ gives $\operatorname{Coll}_z(z = \emptyset)$, so the set $\{\emptyset\} = \mathscr{E}_z(z = \emptyset)$ exists. Thus $\emptyset \neq \{\emptyset\}$ is a theorem. By the rule of existential introduction (Chapter I, § 4, no. 1), we obtain $(\exists y)(\emptyset \neq y)$, and then $(\exists x)(\exists y)(x \neq y)$. Hence $(\exists x)(\exists y)(x \neq y)$ is a theorem.