Theorem nregmodelaxext

Description: The Axiom of Extensionality ax-ext is true in the permutation model defined from F . This theorem is an immediate consequence of the fact that ax-ext holds in all permutation models and is provided as an illustration. (Contributed by Eric Schmidt, 16-Nov-2025)

	Ref	Expression
Hypotheses	nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
	nregmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
Assertion	nregmodelaxext	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\to x=y$$

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
2		nregmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3	1	nregmodelf1o	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
4	3 2	permaxext	$$⊢\forall z\left(zRx\leftrightarrow zRy\right)\to x=y$$