Theorem zfpair 5339

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 axprALT 5340. Instead, use zfpair2 5348 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
zfpair	⊢ {𝑥, 𝑦} ∈ V

Proof of Theorem zfpair

Dummy variables 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfpr2 4577	. 2 ⊢ {𝑥, 𝑦} = {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)}
2		19.43 1886	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)))
3		prlem2 1052	. . . . . 6 ⊢ (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
4	3	exbii 1851	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
5		0ex 5226	. . . . . . . 8 ⊢ ∅ ∈ V
6	5	isseti 3437	. . . . . . 7 ⊢ ∃𝑧 𝑧 = ∅
7		19.41v 1954	. . . . . . 7 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ (∃𝑧 𝑧 = ∅ ∧ 𝑤 = 𝑥))
8	6, 7	mpbiran 705	. . . . . 6 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ 𝑤 = 𝑥)
9		p0ex 5302	. . . . . . . 8 ⊢ {∅} ∈ V
10	9	isseti 3437	. . . . . . 7 ⊢ ∃𝑧 𝑧 = {∅}
11		19.41v 1954	. . . . . . 7 ⊢ (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ (∃𝑧 𝑧 = {∅} ∧ 𝑤 = 𝑦))
12	10, 11	mpbiran 705	. . . . . 6 ⊢ (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)
13	8, 12	orbi12i 911	. . . . 5 ⊢ ((∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦))
14	2, 4, 13	3bitr3ri 301	. . . 4 ⊢ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
15	14	abbii 2809	. . 3 ⊢ {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)} = {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))}
16		dfpr2 4577	. . . . 5 ⊢ {∅, {∅}} = {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})}
17		pp0ex 5304	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrri 2836	. . . 4 ⊢ {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})} ∈ V
19		equequ2 2030	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑥))
20		0inp0 5276	. . . . . . . 8 ⊢ (𝑧 = ∅ → ¬ 𝑧 = {∅})
21	19, 20	prlem1 1051	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (𝑧 = ∅ → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
22	21	alrimdv 1933	. . . . . 6 ⊢ (𝑣 = 𝑥 → (𝑧 = ∅ → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
23	22	spimevw 1999	. . . . 5 ⊢ (𝑧 = ∅ → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
24		orcom 866	. . . . . . . 8 ⊢ (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)))
25		equequ2 2030	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑦))
26	20	con2i 139	. . . . . . . . 9 ⊢ (𝑧 = {∅} → ¬ 𝑧 = ∅)
27	25, 26	prlem1 1051	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑣)))
28	24, 27	syl7bi 254	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
29	28	alrimdv 1933	. . . . . 6 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
30	29	spimevw 1999	. . . . 5 ⊢ (𝑧 = {∅} → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
31	23, 30	jaoi 853	. . . 4 ⊢ ((𝑧 = ∅ ∨ 𝑧 = {∅}) → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
32	18, 31	zfrep4 5215	. . 3 ⊢ {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))} ∈ V
33	15, 32	eqeltri 2835	. 2 ⊢ {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)} ∈ V
34	1, 33	eqeltri 2835	1 ⊢ {𝑥, 𝑦} ∈ V

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  Vcvv 3422  ∅c0 4253  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561

This theorem is referenced by:  axprALT  5340