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 = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
	nregmodel.2	|- R = ( `' F o. _E )
Assertion	nregmodelaxext	|- ( A. z ( z R x <-> z R y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	|- F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
2		nregmodel.2	|- R = ( `' F o. _E )
3	1	nregmodelf1o	|- F : _V -1-1-onto-> _V
4	3 2	permaxext	|- ( A. z ( z R x <-> z R y ) -> x = y )