Theorem en0 8984

Description: The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5312, ax-un 7703. (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 8920	. . . . 5 ⊢ (𝐴 ≈ ∅ → (𝐴 ∈ V ∧ ∅ ∈ V))
2		breng 8921	. . . . 5 ⊢ ((𝐴 ∈ V ∧ ∅ ∈ V) → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅))
3	1, 2	syl 17	. . . 4 ⊢ (𝐴 ≈ ∅ → (𝐴 ≈ ∅ ↔ ∃𝑓 𝑓:𝐴–1-1-onto→∅))
4	3	ibi 269	. . 3 ⊢ (𝐴 ≈ ∅ → ∃𝑓 𝑓:𝐴–1-1-onto→∅)
5		f1ocnv 6804	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→∅ → ◡𝑓:∅–1-1-onto→𝐴)
6		f1o00 6827	. . . . . 6 ⊢ (◡𝑓:∅–1-1-onto→𝐴 ↔ (◡𝑓 = ∅ ∧ 𝐴 = ∅))
7	6	simprbi 500	. . . . 5 ⊢ (◡𝑓:∅–1-1-onto→𝐴 → 𝐴 = ∅)
8	5, 7	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
9	8	exlimiv 1940	. . 3 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→∅ → 𝐴 = ∅)
10	4, 9	syl 17	. 2 ⊢ (𝐴 ≈ ∅ → 𝐴 = ∅)
11		0ex 5247	. . . . 5 ⊢ ∅ ∈ V
12		f1oeq1 6779	. . . . 5 ⊢ (𝑓 = ∅ → (𝑓:∅–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅))
13		f1o0 6829	. . . . 5 ⊢ ∅:∅–1-1-onto→∅
14	11, 12, 13	ceqsexv2d 3493	. . . 4 ⊢ ∃𝑓 𝑓:∅–1-1-onto→∅
15		breng 8921	. . . . 5 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅))
16	11, 11, 15	mp2an 700	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∃𝑓 𝑓:∅–1-1-onto→∅)
17	14, 16	mpbir 233	. . 3 ⊢ ∅ ≈ ∅
18		breq1 5093	. . 3 ⊢ (𝐴 = ∅ → (𝐴 ≈ ∅ ↔ ∅ ≈ ∅))
19	17, 18	mpbiri 260	. 2 ⊢ (𝐴 = ∅ → 𝐴 ≈ ∅)
20	10, 19	impbii 211	1 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1550  ∃wex 1789   ∈ wcel 2132  Vcvv 3444  ∅c0 4276   class class class wbr 5090  ^◡ccnv 5635  –1-1-onto→wf1o 6505   ≈ cen 8909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-mo 2556  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-en 8913

This theorem is referenced by:  0fi  9008  enrefnn  9012  dom0  9062  sdom0  9066  findcard  9117  findcard2  9118  nneneq  9159  cantnff  9615  cantnf0  9616  cantnfp1lem2  9620  cantnflem1  9630  cantnf  9634  cnfcom2lem  9642  cardnueq0  9908  infmap2  10159  fin23lem26  10268  cardeq0  10495  hasheq0  14362  mreexexd  17652  pmtrfmvdn0  19474  pmtrsn  19531  rp-isfinite6  44032  ensucne0OLD  44044