Theorem prclaxpr

Description: A class that is closed under the pairing operation models the Axiom of Pairing ax-pr . Lemma II.2.4(4) of Kunen2 p. 111. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Assertion	prclaxpr	|- ( A. x e. M A. y e. M { x , y } e. M -> A. x e. M A. y e. M E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- w e. _V
2	1	elpr	|- ( w e. { x , y } <-> ( w = x \/ w = y ) )
3	2	biimpri	|- ( ( w = x \/ w = y ) -> w e. { x , y } )
4	3	rgenw	|- A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } )
5		eleq2	|- ( z = { x , y } -> ( w e. z <-> w e. { x , y } ) )
6	5	imbi2d	|- ( z = { x , y } -> ( ( ( w = x \/ w = y ) -> w e. z ) <-> ( ( w = x \/ w = y ) -> w e. { x , y } ) ) )
7	6	ralbidv	|- ( z = { x , y } -> ( A. w e. M ( ( w = x \/ w = y ) -> w e. z ) <-> A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } ) ) )
8	7	rspcev	|- ( ( { x , y } e. M /\ A. w e. M ( ( w = x \/ w = y ) -> w e. { x , y } ) ) -> E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) )
9	4 8	mpan2	|- ( { x , y } e. M -> E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) )
10	9	2ralimi	|- ( A. x e. M A. y e. M { x , y } e. M -> A. x e. M A. y e. M E. z e. M A. w e. M ( ( w = x \/ w = y ) -> w e. z ) )