Theorem permaxpr

Description: The Axiom of Pairing ax-pr 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	permaxpr	|- E. z A. w ( ( w = x \/ w = y ) -> w R z )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	|- F : _V -1-1-onto-> _V
2		permmodel.2	|- R = ( `' F o. _E )
3		fvex	|- ( `' F ` { x , y } ) e. _V
4		breq2	|- ( z = ( `' F ` { x , y } ) -> ( w R z <-> w R ( `' F ` { x , y } ) ) )
5	4	imbi2d	|- ( z = ( `' F ` { x , y } ) -> ( ( ( w = x \/ w = y ) -> w R z ) <-> ( ( w = x \/ w = y ) -> w R ( `' F ` { x , y } ) ) ) )
6	5	albidv	|- ( z = ( `' F ` { x , y } ) -> ( A. w ( ( w = x \/ w = y ) -> w R z ) <-> A. w ( ( w = x \/ w = y ) -> w R ( `' F ` { x , y } ) ) ) )
7		vex	|- w e. _V
8		prex	|- { x , y } e. _V
9	1 2 7 8	brpermmodelcnv	|- ( w R ( `' F ` { x , y } ) <-> w e. { x , y } )
10	7	elpr	|- ( w e. { x , y } <-> ( w = x \/ w = y ) )
11	9 10	sylbbr	|- ( ( w = x \/ w = y ) -> w R ( `' F ` { x , y } ) )
12	11	ax-gen	|- A. w ( ( w = x \/ w = y ) -> w R ( `' F ` { x , y } ) )
13	3 6 12	ceqsexv2d	|- E. z A. w ( ( w = x \/ w = y ) -> w R z )