Theorem zfpair 5420

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 5421. Instead, use zfpair2 5429 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 4648	. 2 ⊢ {𝑥, 𝑦} = {𝑤 ∣ (𝑤 = 𝑥 ∨ 𝑤 = 𝑦)}
2		19.43 1886	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ ∃𝑧(𝑧 = {∅} ∧ 𝑤 = 𝑦)))
3		prlem2 1055	. . . . . 6 ⊢ (((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
4	3	exbii 1851	. . . . 5 ⊢ (∃𝑧((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦)) ↔ ∃𝑧((𝑧 = ∅ ∨ 𝑧 = {∅}) ∧ ((𝑧 = ∅ ∧ 𝑤 = 𝑥) ∨ (𝑧 = {∅} ∧ 𝑤 = 𝑦))))
5		0ex 5308	. . . . . . . 8 ⊢ ∅ ∈ V
6	5	isseti 3490	. . . . . . 7 ⊢ ∃𝑧 𝑧 = ∅
7		19.41v 1954	. . . . . . 7 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ (∃𝑧 𝑧 = ∅ ∧ 𝑤 = 𝑥))
8	6, 7	mpbiran 708	. . . . . 6 ⊢ (∃𝑧(𝑧 = ∅ ∧ 𝑤 = 𝑥) ↔ 𝑤 = 𝑥)
9		p0ex 5383	. . . . . . . 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 4648	. . . . 5 ⊢ {∅, {∅}} = {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})}
17		pp0ex 5385	. . . . 5 ⊢ {∅, {∅}} ∈ V
18	16, 17	eqeltrri 2831	. . . 4 ⊢ {𝑧 ∣ (𝑧 = ∅ ∨ 𝑧 = {∅})} ∈ V
19		equequ2 2030	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝑤 = 𝑣 ↔ 𝑤 = 𝑥))
20		0inp0 5358	. . . . . . . 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 5297	. . 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 4323  {csn 4629  {cpr 4631

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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-pw 4605  df-sn 4630  df-pr 4632

This theorem is referenced by:  axprALT  5421