Theorem zfpair 5415

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 5416. Instead, use zfpair2 5424 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 4643	. 2 ⊢ {𝑥, 𝑦} = {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)}
2		19.43 1886	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)))
3		prlem2 1055	. . . . . 6 ⊢ (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
4	3	exbii 1851	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
5		0ex 5303	. . . . . . . 8 ⊢ ∅ ∈ V
6	5	isseti 3490	. . . . . . 7 ⊢ ∃𝑧 𝑧 = ∅
7		19.41v 1954	. . . . . . 7 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ (∃𝑧 𝑧 = ∅ ∧ 𝑤 = 𝑥))
8	6, 7	mpbiran 708	. . . . . 6 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ 𝑤 = 𝑥)
9		p0ex 5378	. . . . . . . 8 ⊢ {∅} ∈ V
10	9	isseti 3490	. . . . . . 7 ⊢ ∃𝑧 𝑧 = {∅}
11		19.41v 1954	. . . . . . 7 ⊢ (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ (∃𝑧 𝑧 = {∅} ∧ 𝑤 = 𝑦))
12	10, 11	mpbiran 708	. . . . . 6 ⊢ (∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)
13	8, 12	orbi12i 914	. . . . 5 ⊢ ((∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦))
14	2, 4, 13	3bitr3ri 302	. . . 4 ⊢ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
15	14	abbii 2803	. . 3 ⊢ {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)} = {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))}
16		dfpr2 4643	. . . . 5 ⊢ {∅, {∅}} = {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})}
17		pp0ex 5380	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrri 2831	. . . 4 ⊢ {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})} ∈ V
19		equequ2 2030	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑥))
20		0inp0 5353	. . . . . . . 8 ⊢ (𝑧 = ∅ → ¬ 𝑧 = {∅})
21	19, 20	prlem1 1054	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (𝑧 = ∅ → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
22	21	alrimdv 1933	. . . . . 6 ⊢ (𝑣 = 𝑥 → (𝑧 = ∅ → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
23	22	spimevw 1999	. . . . 5 ⊢ (𝑧 = ∅ → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
24		orcom 869	. . . . . . . 8 ⊢ (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)))
25		equequ2 2030	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑦))
26	20	con2i 139	. . . . . . . . 9 ⊢ (𝑧 = {∅} → ¬ 𝑧 = ∅)
27	25, 26	prlem1 1054	. . . . . . . 8 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = {∅} ∧ 𝑤 = 𝑦) ∨ (𝑧 = ∅ ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑣)))
28	24, 27	syl7bi 255	. . . . . . 7 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
29	28	alrimdv 1933	. . . . . 6 ⊢ (𝑣 = 𝑦 → (𝑧 = {∅} → ∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣)))
30	29	spimevw 1999	. . . . 5 ⊢ (𝑧 = {∅} → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
31	23, 30	jaoi 856	. . . 4 ⊢ ((𝑧 = ∅ ∨ 𝑧 = {∅}) → ∃𝑣∀𝑤(((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑣))
32	18, 31	zfrep4 5292	. . 3 ⊢ {𝑤 ∣ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)))} ∈ V
33	15, 32	eqeltri 2830	. 2 ⊢ {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)} ∈ V
34	1, 33	eqeltri 2830	1 ⊢ {𝑥, 𝑦} ∈ V

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 846  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  Vcvv 3475  ∅c0 4320  {csn 4624  {cpr 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-pw 4600  df-sn 4625  df-pr 4627

This theorem is referenced by:  axprALT  5416