Theorem permaxext

Description: The Axiom of Extensionality ax-ext holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	permaxext	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
2		permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3		vex	⊢ 𝑧 ∈ V
4		vex	⊢ 𝑥 ∈ V
5	1 2 3 4	brpermmodel	⊢ ( 𝑧 𝑅 𝑥 ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) )
6		vex	⊢ 𝑦 ∈ V
7	1 2 3 6	brpermmodel	⊢ ( 𝑧 𝑅 𝑦 ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑦 ) )
8	5 7	bibi12i	⊢ ( ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑦 ) ) )
9	8	albii	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑦 ) ) )
10		dfcleq	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑦 ) ) )
11	9 10	bitr4i	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
12		f1of1	⊢ ( 𝐹 : V –1-1-onto→ V → 𝐹 : V –1-1→ V )
13	1 12	ax-mp	⊢ 𝐹 : V –1-1→ V
14		f1veqaeq	⊢ ( ( 𝐹 : V –1-1→ V ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15	13 14	mpan	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16	15	el2v	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 )
17	11 16	sylbi	⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 𝑦 ) → 𝑥 = 𝑦 )