Axiom ax-pr 2785

Description: The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 2784 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.

Assertion

Ref	Expression
ax-pr	|- E.zA.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	. . . . . . 7 set w
2	1	cv 957	. . . . . 6 class w
3		vx	. . . . . . 7 set x
4	3	cv 957	. . . . . 6 class x
5	2, 4	wceq 958	. . . . 5 wff w = x
6		vy	. . . . . . 7 set y
7	6	cv 957	. . . . . 6 class y
8	2, 7	wceq 958	. . . . 5 wff w = y
9	5, 8	wo 222	. . . 4 wff (w = x \/ w = y)
10		vz	. . . . . 6 set z
11	10	cv 957	. . . . 5 class z
12	2, 11	wcel 960	. . . 4 wff w e. z
13	9, 12	wi 3	. . 3 wff ((w = x \/ w = y) -> w e. z)
14	13, 1	wal 956	. 2 wff A.w((w = x \/ w = y) -> w e. z)
15	14, 10	wex 982	1 wff E.zA.w((w = x \/ w = y) -> w e. z)

This axiom is referenced by:  zfpair2 2786

Copyright terms: Public domain