Theorem en0 8564

Description: The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.)

Assertion

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

Proof of Theorem en0

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bren 8510	. . 3 ⊢ (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅)
2		f1ocnv 6620	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→∅ → ◡𝑓:∅–1-1-onto→𝐴)
3		f1o00 6642	. . . . . 6 ⊢ (◡𝑓:∅–1-1-onto→𝐴 ↔ (◡𝑓 = ∅ ∧ 𝐴 = ∅))
4	3	simprbi 499	. . . . 5 ⊢ (◡𝑓:∅–1-1-onto→𝐴 → 𝐴 = ∅)
5	2, 4	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
6	5	exlimiv 1925	. . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
7	1, 6	sylbi 219	. 2 ⊢ (𝐴 ≈ ∅ → 𝐴 = ∅)
8		0ex 5202	. . . 4 ⊢ ∅ ∈ V
9	8	enref 8534	. . 3 ⊢ ∅ ≈ ∅
10		breq1 5060	. . 3 ⊢ (𝐴 = ∅ → (𝐴 ≈ ∅ ↔ ∅ ≈ ∅))
11	9, 10	mpbiri 260	. 2 ⊢ (𝐴 = ∅ → 𝐴 ≈ ∅)
12	7, 11	impbii 211	1 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 208   = wceq 1531  ∃wex 1774  ∅c0 4289   class class class wbr 5057  ^◡ccnv 5547  –1-1-onto→wf1o 6347   ≈ cen 8498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-en 8502

This theorem is referenced by:  snfi  8586  dom0  8637  0sdomg  8638  nneneq  8692  snnen2o  8699  enp1i  8745  findcard  8749  findcard2  8750  fiint  8787  cantnff  9129  cantnf0  9130  cantnfp1lem2  9134  cantnflem1  9144  cantnf  9148  cnfcom2lem  9156  cardnueq0  9385  infmap2  9632  fin23lem26  9739  cardeq0  9966  hasheq0  13716  mreexexd  16911  pmtrfmvdn0  18582  pmtrsn  18639  rp-isfinite6  39875  ensucne0  39886  ensucne0OLD  39887