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	|- F : _V -1-1-onto-> _V
	permmodel.2	|- R = ( `' F o. _E )
Assertion	permaxext	|- ( A. z ( z R x <-> z R y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	|- F : _V -1-1-onto-> _V
2		permmodel.2	|- R = ( `' F o. _E )
3		vex	|- z e. _V
4		vex	|- x e. _V
5	1 2 3 4	brpermmodel	|- ( z R x <-> z e. ( F ` x ) )
6		vex	|- y e. _V
7	1 2 3 6	brpermmodel	|- ( z R y <-> z e. ( F ` y ) )
8	5 7	bibi12i	|- ( ( z R x <-> z R y ) <-> ( z e. ( F ` x ) <-> z e. ( F ` y ) ) )
9	8	albii	|- ( A. z ( z R x <-> z R y ) <-> A. z ( z e. ( F ` x ) <-> z e. ( F ` y ) ) )
10		dfcleq	|- ( ( F ` x ) = ( F ` y ) <-> A. z ( z e. ( F ` x ) <-> z e. ( F ` y ) ) )
11	9 10	bitr4i	|- ( A. z ( z R x <-> z R y ) <-> ( F ` x ) = ( F ` y ) )
12		f1of1	|- ( F : _V -1-1-onto-> _V -> F : _V -1-1-> _V )
13	1 12	ax-mp	|- F : _V -1-1-> _V
14		f1veqaeq	|- ( ( F : _V -1-1-> _V /\ ( x e. _V /\ y e. _V ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
15	13 14	mpan	|- ( ( x e. _V /\ y e. _V ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
16	15	el2v	|- ( ( F ` x ) = ( F ` y ) -> x = y )
17	11 16	sylbi	|- ( A. z ( z R x <-> z R y ) -> x = y )