Axiom ax-pr 4187

Description: The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4103). (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 1491	. . . . 5 wff w = x
4		vy	. . . . . 6 setvar y
5	1, 4	weq 1491	. . . . 5 wff w = y
6	3, 5	wo 698	. . . 4 wff ( w = x \/ w = y )
7		vz	. . . . 5 setvar z
8	1, 7	wel 2137	. . . 4 wff w e. z
9	6, 8	wi 4	. . 3 wff ( ( w = x \/ w = y ) -> w e. z )
10	9, 1	wal 1341	. 2 wff A. w ( ( w = x \/ w = y ) -> w e. z )
11	10, 7	wex 1480	1 wff E. z A. w ( ( w = x \/ w = y ) -> w e. z )

This axiom is referenced by:  zfpair2  4188  bj-zfpair2  13792