zfpair - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zfpair 2766

Description: The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axpr 2767. Instead, use zfpair2 2769 below so that the uses of the Axiom of Pairing can be more easily identified.

**Assertion**
Ref	Expression
zfpair	⊢ {x, y} ∈ V

**Proof of Theorem zfpair**
Step	Hyp	Ref	Expression
1		dfpr2 2411	. 2 ⊢ {x, y} = {w∣(w = x ⋁ w = y)}
2		19.43 1084	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ (∃z(z = ∅ ⋀ w = x) ⋁ ∃z(z = {∅} ⋀ w = y)))
3		prlem2 769	. . . . . 6 ⊢ (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
4	3	exbii 1047	. . . . 5 ⊢ (∃z((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
5		19.41v 1299	. . . . . . 7 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ (∃z z = ∅ ⋀ w = x))
6		0ex 2700	. . . . . . . 8 ⊢ ∅ ∈ V
7	6	isseti 1805	. . . . . . 7 ⊢ ∃z z = ∅
8	5, 7	mpbiran 726	. . . . . 6 ⊢ (∃z(z = ∅ ⋀ w = x) ↔ w = x)
9		19.41v 1299	. . . . . . 7 ⊢ (∃z(z = {∅} ⋀ w = y) ↔ (∃z z = {∅} ⋀ w = y))
10		p0ex 2759	. . . . . . . 8 ⊢ {∅} ∈ V
11	10	isseti 1805	. . . . . . 7 ⊢ ∃z z = {∅}
12	9, 11	mpbiran 726	. . . . . 6 ⊢ (∃z(z = {∅} ⋀ w = y) ↔ w = y)
13	8, 12	orbi12i 257	. . . . 5 ⊢ ((∃z(z = ∅ ⋀ w = x) ⋁ ∃z(z = {∅} ⋀ w = y)) ↔ (w = x ⋁ w = y))
14	2, 4, 13	3bitr3r 182	. . . 4 ⊢ ((w = x ⋁ w = y) ↔ ∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y))))
15	14	abbii 1566	. . 3 ⊢ {w∣(w = x ⋁ w = y)} = {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))}
16		dfpr2 2411	. . . . 5 ⊢ {∅, {∅}} = {z∣(z = ∅ ⋁ z = {∅})}
17		pp0ex 2760	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrr 1536	. . . 4 ⊢ {z∣(z = ∅ ⋁ z = {∅})} ∈ V
19		equequ2 1131	. . . . . . . 8 ⊢ (v = x → (w = v ↔ w = x))
20		0inp0 2727	. . . . . . . 8 ⊢ (z = ∅ → ¬ z = {∅})
21	19, 20	prlem1 768	. . . . . . 7 ⊢ (v = x → (z = ∅ → (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
22	21	19.21adv 1282	. . . . . 6 ⊢ (v = x → (z = ∅ → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
23	22	a4imev 1267	. . . . 5 ⊢ (z = ∅ → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
24		equequ2 1131	. . . . . . . . 9 ⊢ (v = y → (w = v ↔ w = y))
25	20	con2i 97	. . . . . . . . 9 ⊢ (z = {∅} → ¬ z = ∅)
26	24, 25	prlem1 768	. . . . . . . 8 ⊢ (v = y → (z = {∅} → (((z = {∅} ⋀ w = y) ⋁ (z = ∅ ⋀ w = x)) → w = v)))
27		orcom 246	. . . . . . . 8 ⊢ (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) ↔ ((z = {∅} ⋀ w = y) ⋁ (z = ∅ ⋀ w = x)))
28	26, 27	syl7ib 216	. . . . . . 7 ⊢ (v = y → (z = {∅} → (((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
29	28	19.21adv 1282	. . . . . 6 ⊢ (v = y → (z = {∅} → ∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v)))
30	29	a4imev 1267	. . . . 5 ⊢ (z = {∅} → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
31	23, 30	jaoi 341	. . . 4 ⊢ ((z = ∅ ⋁ z = {∅}) → ∃v∀w(((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)) → w = v))
32	18, 31	zfrep4 2690	. . 3 ⊢ {w∣∃z((z = ∅ ⋁ z = {∅}) ⋀ ((z = ∅ ⋀ w = x) ⋁ (z = {∅} ⋀ w = y)))} ∈ V
33	15, 32	eqeltr 1535	. 2 ⊢ {w∣(w = x ⋁ w = y)} ∈ V
34	1, 33	eqeltr 1535	1 ⊢ {x, y} ∈ V

Colors of variables: wff set class

Syntax hints: → wi 3 ⋁ wo 222 ⋀ wa 223 ∀wal 951 = wceq 953 ∈ wcel 955 ∃wex 977 {cab 1455 Vcvv 1801 ∅c0 2269 {csn 2398 {cpr 2399

This theorem is referenced by: axpr 2767

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1451 ax-rep 2682 ax-sep 2692 ax-nul 2699 ax-pow 2731

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1374 df-mo 1375 df-clab 1456 df-cleq 1461 df-clel 1464 df-ne 1578 df-v 1802 df-dif 2038 df-un 2039 df-in 2040 df-ss 2042 df-nul 2270 df-pw 2391 df-sn 2401 df-pr 2402