Theorem wfaxpr

Description: The class of well-founded sets models the Axiom of Pairing ax-pr . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	|- W = U. ( R1 " On )
Assertion	wfaxpr	|- A. x e. W A. y e. W E. z e. W A. w e. W ( ( w = x \/ w = y ) -> w e. z )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		prwf	|- ( ( x e. U. ( R1 " On ) /\ y e. U. ( R1 " On ) ) -> { x , y } e. U. ( R1 " On ) )
3	1	eleq2i	|- ( x e. W <-> x e. U. ( R1 " On ) )
4	1	eleq2i	|- ( y e. W <-> y e. U. ( R1 " On ) )
5	3 4	anbi12i	|- ( ( x e. W /\ y e. W ) <-> ( x e. U. ( R1 " On ) /\ y e. U. ( R1 " On ) ) )
6	1	eleq2i	|- ( { x , y } e. W <-> { x , y } e. U. ( R1 " On ) )
7	2 5 6	3imtr4i	|- ( ( x e. W /\ y e. W ) -> { x , y } e. W )
8	7	rgen2	|- A. x e. W A. y e. W { x , y } e. W
9		prclaxpr	|- ( A. x e. W A. y e. W { x , y } e. W -> A. x e. W A. y e. W E. z e. W A. w e. W ( ( w = x \/ w = y ) -> w e. z ) )
10	8 9	ax-mp	|- A. x e. W A. y e. W E. z e. W A. w e. W ( ( w = x \/ w = y ) -> w e. z )