Axiom ax-pr 5346

Description: The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5345 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	⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

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 1971	. . . . 5 wff 𝑤 = 𝑥
4		vy	. . . . . 6 setvar 𝑦
5	1, 4	weq 1971	. . . . 5 wff 𝑤 = 𝑦
6	3, 5	wo 847	. . . 4 wff (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)
7		vz	. . . . 5 setvar 𝑧
8	1, 7	wel 2113	. . . 4 wff 𝑤 ∈ 𝑧
9	6, 8	wi 4	. . 3 wff ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
10	9, 1	wal 1541	. 2 wff ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
11	10, 7	wex 1787	1 wff ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

This axiom is referenced by:  zfpair2  5347