Theorem zfpair 2745

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 2746. Instead, use zfpair2 2748 below so that the uses of the Axiom of Pairing can be more easily identified.

Assertion

Ref	Expression
zfpair	|- {x, y} e. V

Proof of Theorem zfpair

Step	Hyp	Ref	Expression
1		dfpr2 2393	. 2 |- {x, y} = {w | (w = x \/ w = y)}
2		19.43 1064	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> (E.z(z = (/) /\ w = x) \/ E.z(z = {(/)} /\ w = y)))
3		prlem2 768	. . . . . 6 |- (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> ((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
4	3	exbii 1027	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
5		19.41v 1287	. . . . . . 7 |- (E.z(z = (/) /\ w = x) <-> (E.z z = (/) /\ w = x))
6		0ex 2679	. . . . . . . 8 |- (/) e. V
7	6	isseti 1790	. . . . . . 7 |- E.z z = (/)
8	5, 7	mpbiran 725	. . . . . 6 |- (E.z(z = (/) /\ w = x) <-> w = x)
9		19.41v 1287	. . . . . . 7 |- (E.z(z = {(/)} /\ w = y) <-> (E.z z = {(/)} /\ w = y))
10		p0ex 2738	. . . . . . . 8 |- {(/)} e. V
11	10	isseti 1790	. . . . . . 7 |- E.z z = {(/)}
12	9, 11	mpbiran 725	. . . . . 6 |- (E.z(z = {(/)} /\ w = y) <-> w = y)
13	8, 12	orbi12i 257	. . . . 5 |- ((E.z(z = (/) /\ w = x) \/ E.z(z = {(/)} /\ w = y)) <-> (w = x \/ w = y))
14	2, 4, 13	3bitr3r 182	. . . 4 |- ((w = x \/ w = y) <-> E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
15	14	abbii 1551	. . 3 |- {w | (w = x \/ w = y)} = {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))}
16		dfpr2 2393	. . . . 5 |- {(/), {(/)}} = {z | (z = (/) \/ z = {(/)})}
17		pp0ex 2739	. . . . 5 |- {(/), {(/)}} e. V
18	16, 17	eqeltrr 1521	. . . 4 |- {z | (z = (/) \/ z = {(/)})} e. V
19		equequ2 1122	. . . . . . . 8 |- (v = x -> (w = v <-> w = x))
20		0inp0 2706	. . . . . . . 8 |- (z = (/) -> -. z = {(/)})
21	19, 20	prlem1 767	. . . . . . 7 |- (v = x -> (z = (/) -> (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
22	21	19.21adv 1270	. . . . . 6 |- (v = x -> (z = (/) -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
23	22	a4w 1255	. . . . 5 |- (z = (/) -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
24		equequ2 1122	. . . . . . . . 9 |- (v = y -> (w = v <-> w = y))
25	20	con2i 97	. . . . . . . . 9 |- (z = {(/)} -> -. z = (/))
26	24, 25	prlem1 767	. . . . . . . 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 1270	. . . . . 6 |- (v = y -> (z = {(/)} -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
30	29	a4w 1255	. . . . 5 |- (z = {(/)} -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
31	23, 30	jaoi 341	. . . 4 |- ((z = (/) \/ z = {(/)}) -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
32	18, 31	zfrep4 2669	. . 3 |- {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))} e. V
33	15, 32	eqeltr 1520	. 2 |- {w | (w = x \/ w = y)} e. V
34	1, 33	eqeltr 1520	1 |- {x, y} e. V

Syntax hints:   -> wi 3   \/ wo 222   /\ wa 223  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105  {cab 1440  Vcvv 1786  (/)c0 2251  {csn 2380  {cpr 2381

This theorem is referenced by:  axpr 2746

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384

Copyright terms: Public domain