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. (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)$$