Theorem zfpair 3337

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 3338. Instead, use zfpair2 3340 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 2883	. 2 |- {x, y} = {w | (w = x \/ w = y)}
2		19.43 1278	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> (E.z(z = (/) /\ w = x) \/ E.z(z = {(/)} /\ w = y)))
3		prlem2 847	. . . . . 6 |- (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> ((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
4	3	exbii 1236	. . . . 5 |- (E.z((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
5		19.41v 1523	. . . . . . 7 |- (E.z(z = (/) /\ w = x) <-> (E.z z = (/) /\ w = x))
6		0ex 3261	. . . . . . . 8 |- (/) e. _V
7	6	isseti 2130	. . . . . . 7 |- E.z z = (/)
8	5, 7	mpbiran 795	. . . . . 6 |- (E.z(z = (/) /\ w = x) <-> w = x)
9		19.41v 1523	. . . . . . 7 |- (E.z(z = {(/)} /\ w = y) <-> (E.z z = {(/)} /\ w = y))
10		p0ex 3310	. . . . . . . 8 |- {(/)} e. _V
11	10	isseti 2130	. . . . . . 7 |- E.z z = {(/)}
12	9, 11	mpbiran 795	. . . . . 6 |- (E.z(z = {(/)} /\ w = y) <-> w = y)
13	8, 12	orbi12i 275	. . . . 5 |- ((E.z(z = (/) /\ w = x) \/ E.z(z = {(/)} /\ w = y)) <-> (w = x \/ w = y))
14	2, 4, 13	3bitr3ri 198	. . . 4 |- ((w = x \/ w = y) <-> E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y))))
15	14	abbii 1843	. . 3 |- {w | (w = x \/ w = y)} = {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))}
16		dfpr2 2883	. . . . 5 |- {(/), {(/)}} = {z | (z = (/) \/ z = {(/)})}
17		pp0ex 3311	. . . . 5 |- {(/), {(/)}} e. _V
18	16, 17	eqeltrri 1805	. . . 4 |- {z | (z = (/) \/ z = {(/)})} e. _V
19		equequ2 1333	. . . . . . . 8 |- (v = x -> (w = v <-> w = x))
20		0inp0 3290	. . . . . . . 8 |- (z = (/) -> -. z = {(/)})
21	19, 20	prlem1 845	. . . . . . 7 |- (v = x -> (z = (/) -> (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
22	21	19.21adv 1504	. . . . . 6 |- (v = x -> (z = (/) -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
23	22	a4imev 1488	. . . . 5 |- (z = (/) -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
24		equequ2 1333	. . . . . . . . 9 |- (v = y -> (w = v <-> w = y))
25	20	con2i 112	. . . . . . . . 9 |- (z = {(/)} -> -. z = (/))
26	24, 25	prlem1 845	. . . . . . . 8 |- (v = y -> (z = {(/)} -> (((z = {(/)} /\ w = y) \/ (z = (/) /\ w = x)) -> w = v)))
27		orcom 264	. . . . . . . 8 |- (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) <-> ((z = {(/)} /\ w = y) \/ (z = (/) /\ w = x)))
28	26, 27	syl7ib 232	. . . . . . 7 |- (v = y -> (z = {(/)} -> (((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
29	28	19.21adv 1504	. . . . . 6 |- (v = y -> (z = {(/)} -> A.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v)))
30	29	a4imev 1488	. . . . 5 |- (z = {(/)} -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
31	23, 30	jaoi 366	. . . 4 |- ((z = (/) \/ z = {(/)}) -> E.vA.w(((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)) -> w = v))
32	18, 31	zfrep4 3251	. . 3 |- {w | E.z((z = (/) \/ z = {(/)}) /\ ((z = (/) /\ w = x) \/ (z = {(/)} /\ w = y)))} e. _V
33	15, 32	eqeltri 1804	. 2 |- {w | (w = x \/ w = y)} e. _V
34	1, 33	eqeltri 1804	1 |- {x, y} e. _V

Syntax hints:   -> wi 3   \/ wo 238   /\ wa 239  A.wal 1134   = wceq 1136   e. wcel 1138  E.wex 1164  {cab 1708  _Vcvv 2125  (/)c0 2701  {csn 2868  {cpr 2869

This theorem is referenced by:  axpr 3338  dfdir2 14365  latdir 14369  clatlat 16650

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874

Copyright terms: Public domain