Theorem en0 8591

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

Assertion

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

Proof of Theorem en0

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 8537	. . 3 ⊢ (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅)
2		f1ocnv 6615	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→∅ → ◡𝑓:∅–1-1-onto→𝐴)
3		f1o00 6637	. . . . . 6 ⊢ (◡𝑓:∅–1-1-onto→𝐴 ↔ (◡𝑓 = ∅ ∧ 𝐴 = ∅))
4	3	simprbi 501	. . . . 5 ⊢ (◡𝑓:∅–1-1-onto→𝐴 → 𝐴 = ∅)
5	2, 4	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
6	5	exlimiv 1932	. . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
7	1, 6	sylbi 220	. 2 ⊢ (𝐴 ≈ ∅ → 𝐴 = ∅)
8		0ex 5178	. . . . 5 ⊢ ∅ ∈ V
9		f1oeq1 6591	. . . . 5 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅))
10		f1o0 6639	. . . . 5 ⊢ ∅:∅–1-1-onto→∅
11	8, 9, 10	ceqsexv2d 3460	. . . 4 ⊢ ∃𝑓 𝑓:∅–1-1-onto→∅
12		bren 8537	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅)
13	11, 12	mpbir 234	. . 3 ⊢ ∅ ≈ ∅
14		breq1 5036	. . 3 ⊢ (𝐴 = ∅ → (𝐴 ≈ ∅ ↔ ∅ ≈ ∅))
15	13, 14	mpbiri 261	. 2 ⊢ (𝐴 = ∅ → 𝐴 ≈ ∅)
16	7, 15	impbii 212	1 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 209   = wceq 1539  ∃wex 1782  ∅c0 4226   class class class wbr 5033  ^◡ccnv 5524  –1-1-onto→wf1o 6335   ≈ cen 8525

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-en 8529

This theorem is referenced by:  snfi  8615  enrefnn  8618  dom0  8668  0sdomg  8669  nneneq  8723  snnen2o  8730  findcard  8735  findcard2  8736  enp1i  8790  findcard2OLD  8794  fiint  8829  cantnff  9171  cantnf0  9172  cantnfp1lem2  9176  cantnflem1  9186  cantnf  9190  cnfcom2lem  9198  cardnueq0  9427  infmap2  9679  fin23lem26  9786  cardeq0  10013  hasheq0  13775  mreexexd  16978  pmtrfmvdn0  18658  pmtrsn  18715  rp-isfinite6  40600  ensucne0  40611  ensucne0OLD  40612