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	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
	nregmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	nregmodelaxext	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
2		nregmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3	1	nregmodelf1o	⊢ 𝐹 : V –1-1-onto→ V
4	3 2	permaxext	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) → 𝑥 = 𝑦 )