Axiom ax-pr 4906

Description: The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 4905 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.)

Assertion

Ref	Expression
ax-pr	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Distinct variable groups:   x, z, w   y, z, w

Detailed syntax breakdown of Axiom ax-pr

Step	Hyp	Ref	Expression
1		vw	. . . . . 6 setvar w
2		vx	. . . . . 6 setvar x
3	1, 2	weq 1874	. . . . 5 wff w = x
4		vy	. . . . . 6 setvar y
5	1, 4	weq 1874	. . . . 5 wff w = y
6	3, 5	wo 383	. . . 4 wff ( w = x \/ w = y )
7		vz	. . . . 5 setvar z
8	1, 7	wel 1991	. . . 4 wff w e. z
9	6, 8	wi 4	. . 3 wff ( ( w = x \/ w = y ) -> w e. z )
10	9, 1	wal 1481	. 2 wff A. w ( ( w = x \/ w = y ) -> w e. z )
11	10, 7	wex 1704	1 wff E. z A. w ( ( w = x \/ w = y ) -> w e. z )

This axiom is referenced by:  zfpair2  4907