Axiom ax-pr 4186

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

Assertion

Ref	Expression
ax-pr	⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Distinct variable groups:   𝑥,𝑧,𝑤   𝑦,𝑧,𝑤

Detailed syntax breakdown of Axiom ax-pr

Step	Hyp	Ref	Expression
1		vw	. . . . . 6 setvar 𝑤
2		vx	. . . . . 6 setvar 𝑥
3	1, 2	weq 1491	. . . . 5 wff 𝑤 = 𝑥
4		vy	. . . . . 6 setvar 𝑦
5	1, 4	weq 1491	. . . . 5 wff 𝑤 = 𝑦
6	3, 5	wo 698	. . . 4 wff (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)
7		vz	. . . . 5 setvar 𝑧
8	1, 7	wel 2137	. . . 4 wff 𝑤 ∈ 𝑧
9	6, 8	wi 4	. . 3 wff ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
10	9, 1	wal 1341	. 2 wff ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
11	10, 7	wex 1480	1 wff ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

This axiom is referenced by:  zfpair2  4187  bj-zfpair2  13752