Theorem zfpair 2783

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 2784. Instead, use zfpair2 2786 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 2426	. 2 |- {x, y} = {w | (w = x \/ w = y)}
2		19.43 1090	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> (E.z(z = (/) /\ w = x) \/ E.z(z = {(/)} /\ w = y)))
3		prlem2 773	. . . . . 6 |- (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> ((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
4	3	exbii 1053	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
5		19.41v 1307	. . . . . . 7 |- (E.z(z = (/) /\ w = x) <-> (E.z z = (/) /\ w = x))
6		0ex 2716	. . . . . . . 8 |- (/) e. V
7	6	isseti 1818	. . . . . . 7 |- E.z z = (/)
8	5, 7	mpbiran 730	. . . . . 6 |- (E.z(z = (/) /\ w = x) <-> w = x)
9		19.41v 1307	. . . . . . 7 |- (E.z(z = {(/)} /\ w = y) <-> (E.z z = {(/)} /\ w = y))
10		p0ex 2776	. . . . . . . 8 |- {(/)} e. V
11	10	isseti 1818	. . . . . . 7 |- E.z z = {(/)}
12	9, 11	mpbiran 730	. . . . . 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 1578	. . 3 |- {w | (w = x \/ w = y)} = {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))}
16		dfpr2 2426	. . . . 5 |- {(/), {(/)}} = {z | (z = (/) \/ z = {(/)})}
17		pp0ex 2777	. . . . 5 |- {(/), {(/)}} e. V
18	16, 17	eqeltrr 1548	. . . 4 |- {z | (z = (/) \/ z = {(/)})} e. V
19		equequ2 1137	. . . . . . . 8 |- (v = x -> (w = v <-> w = x))
20		0inp0 2743	. . . . . . . 8 |- (z = (/) -> -. z = {(/)})
21	19, 20	prlem1 772	. . . . . . 7 |- (v = x -> (z = (/) -> (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
22	21	19.21adv 1290	. . . . . 6 |- (v = x -> (z = (/) -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
23	22	a4imev 1275	. . . . 5 |- (z = (/) -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
24		equequ2 1137	. . . . . . . . 9 |- (v = y -> (w = v <-> w = y))
25	20	con2i 97	. . . . . . . . 9 |- (z = {(/)} -> -. z = (/))
26	24, 25	prlem1 772	. . . . . . . 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 1290	. . . . . 6 |- (v = y -> (z = {(/)} -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
30	29	a4imev 1275	. . . . 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 2706	. . 3 |- {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))} e. V
33	15, 32	eqeltr 1547	. 2 |- {w | (w = x \/ w = y)} e. V
34	1, 33	eqeltr 1547	1 |- {x, y} e. V

Syntax hints:   -> wi 3   \/ wo 222   /\ wa 223  A.wal 956   = wceq 958   e. wcel 960  E.wex 982  {cab 1466  Vcvv 1814  (/)c0 2283  {csn 2413  {cpr 2414

This theorem is referenced by:  axpr 2784

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417

Copyright terms: Public domain