Theorem en0 8803

Description: The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5288, ax-un 7588. (Revised by BTernaryTau, 23-Sep-2024.)

Assertion

Ref	Expression
en0	⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)

Proof of Theorem en0

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		encv 8741	. . . . 5 ⊢ (𝐴 ≈ ∅ → (𝐴 ∈ V ∧ ∅ ∈ V))
2		breng 8742	. . . . 5 ⊢ ((𝐴 ∈ V ∧ ∅ ∈ V) → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅))
3	1, 2	syl 17	. . . 4 ⊢ (𝐴 ≈ ∅ → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅))
4	3	ibi 266	. . 3 ⊢ (𝐴 ≈ ∅ → ∃𝑓 𝑓:𝐴–1-1-onto→∅)
5		f1ocnv 6728	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→∅ → ◡𝑓:∅–1-1-onto→𝐴)
6		f1o00 6751	. . . . . 6 ⊢ (◡𝑓:∅–1-1-onto→𝐴 ↔ (◡𝑓 = ∅ ∧ 𝐴 = ∅))
7	6	simprbi 497	. . . . 5 ⊢ (◡𝑓:∅–1-1-onto→𝐴 → 𝐴 = ∅)
8	5, 7	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
9	8	exlimiv 1933	. . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
10	4, 9	syl 17	. 2 ⊢ (𝐴 ≈ ∅ → 𝐴 = ∅)
11		0ex 5231	. . . . 5 ⊢ ∅ ∈ V
12		f1oeq1 6704	. . . . 5 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅))
13		f1o0 6753	. . . . 5 ⊢ ∅:∅–1-1-onto→∅
14	11, 12, 13	ceqsexv2d 3481	. . . 4 ⊢ ∃𝑓 𝑓:∅–1-1-onto→∅
15		breng 8742	. . . . 5 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅))
16	11, 11, 15	mp2an 689	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅)
17	14, 16	mpbir 230	. . 3 ⊢ ∅ ≈ ∅
18		breq1 5077	. . 3 ⊢ (𝐴 = ∅ → (𝐴 ≈ ∅ ↔ ∅ ≈ ∅))
19	17, 18	mpbiri 257	. 2 ⊢ (𝐴 = ∅ → 𝐴 ≈ ∅)
20	10, 19	impbii 208	1 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432  ∅c0 4256   class class class wbr 5074  ^◡ccnv 5588  –1-1-onto→wf1o 6432   ≈ cen 8730

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-en 8734

This theorem is referenced by:  snfi  8834  enrefnn  8837  dom0  8889  dom0OLD  8890  0sdomgOLD  8892  sdom0  8895  findcard  8946  findcard2  8947  nneneq  8992  nneneqOLD  9004  snnen2oOLD  9010  enp1i  9052  findcard2OLD  9056  fiint  9091  cantnff  9432  cantnf0  9433  cantnfp1lem2  9437  cantnflem1  9447  cantnf  9451  cnfcom2lem  9459  cardnueq0  9722  infmap2  9974  fin23lem26  10081  cardeq0  10308  hasheq0  14078  mreexexd  17357  pmtrfmvdn0  19070  pmtrsn  19127  rp-isfinite6  41125  ensucne0  41136  ensucne0OLD  41137