Axiom ax-pr 3917

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 3851). (Contributed by NM, 14-Nov-2006.)

Assertion

Ref	Expression
ax-pr	⊢ ∃z∀w((w = x ∨ w = y) → w ∈ 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 1374	. . . . 5 wff w = x
4		vy	. . . . . 6 setvar y
5	1, 4	weq 1374	. . . . 5 wff w = y
6	3, 5	wo 616	. . . 4 wff (w = x ∨ w = y)
7		vz	. . . . 5 setvar z
8	1, 7	wel 1376	. . . 4 wff w ∈ z
9	6, 8	wi 4	. . 3 wff ((w = x ∨ w = y) → w ∈ z)
10	9, 1	wal 1226	. 2 wff ∀w((w = x ∨ w = y) → w ∈ z)
11	10, 7	wex 1363	1 wff ∃z∀w((w = x ∨ w = y) → w ∈ z)

This axiom is referenced by:  zfpair2  3918  bj-zfpair2  6477