Axiom ax-pr 2769

Description: The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 2768 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	⊢ ∃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	. . . . . . 7 set w
2	1	cv 952	. . . . . 6 class w
3		vx	. . . . . . 7 set x
4	3	cv 952	. . . . . 6 class x
5	2, 4	wceq 953	. . . . 5 wff w = x
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8	2, 7	wceq 953	. . . . 5 wff w = y
9	5, 8	wo 222	. . . 4 wff (w = x ⋁ w = y)
10		vz	. . . . . 6 set z
11	10	cv 952	. . . . 5 class z
12	2, 11	wcel 955	. . . 4 wff w ∈ z
13	9, 12	wi 3	. . 3 wff ((w = x ⋁ w = y) → w ∈ z)
14	13, 1	wal 951	. 2 wff ∀w((w = x ⋁ w = y) → w ∈ z)
15	14, 10	wex 977	1 wff ∃z∀w((w = x ⋁ w = y) → w ∈ z)

This axiom is referenced by:  zfpair2 2770

Copyright terms: Public domain