Theorem wfaxext

Description: The class of well-founded sets models the Axiom of Extensionality ax-ext . Part of Corollary II.2.5 of Kunen2 p. 112.

This is the first of a series of theorems showing that all the axioms of ZFC hold in the class of well-founded sets, which we here denote by W . More precisely, for each axiom of ZFC, we obtain a provable statement if we restrict all quantifiers to W (including implicit universal quantifiers on free variables).

None of these proofs use the Axiom of Regularity. In particular, the Axiom of Regularity itself is proved to hold in W without using Regularity. Further, the Axiom of Choice is used only in the proof that Choice holds in W . This has the consequence that any theorem of ZF (possibly proved using Regularity) can be proved, without using Regularity, to hold in W . This gives us a relative consistency result: If ZF without Regularity is consistent, so is ZF itself. Similarly, if ZFC without Regularity is consistent, so is ZFC itself. These consistency results are metatheorems and are part of Theorem II.2.13 of Kunen2 p. 114.

(Contributed by Eric Schmidt, 11-Sep-2025) (Revised by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
Assertion	wfaxext	$$⊢\forall x\in W\forall y\in W\left(\forall z\in W\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
2		trwf	$$⊢\mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
3		treq	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]\to \left(\mathrm{Tr}W\leftrightarrow \mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]\right)$$
4	1 3	ax-mp	$$⊢\mathrm{Tr}W\leftrightarrow \mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
5	2 4	mpbir	$$⊢\mathrm{Tr}W$$
6		traxext	$$⊢\mathrm{Tr}W\to \forall x\in W\forall y\in W\left(\forall z\in W\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$
7	5 6	ax-mp	$$⊢\forall x\in W\forall y\in W\left(\forall z\in W\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$