Metamath Proof Explorer


Theorem en0

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

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

Proof

Step Hyp Ref Expression
1 bren ( 𝐴 ≈ ∅ ↔ ∃ 𝑓 𝑓 : 𝐴1-1-onto→ ∅ )
2 f1ocnv ( 𝑓 : 𝐴1-1-onto→ ∅ → 𝑓 : ∅ –1-1-onto𝐴 )
3 f1o00 ( 𝑓 : ∅ –1-1-onto𝐴 ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
4 3 simprbi ( 𝑓 : ∅ –1-1-onto𝐴𝐴 = ∅ )
5 2 4 syl ( 𝑓 : 𝐴1-1-onto→ ∅ → 𝐴 = ∅ )
6 5 exlimiv ( ∃ 𝑓 𝑓 : 𝐴1-1-onto→ ∅ → 𝐴 = ∅ )
7 1 6 sylbi ( 𝐴 ≈ ∅ → 𝐴 = ∅ )
8 0ex ∅ ∈ V
9 8 enref ∅ ≈ ∅
10 breq1 ( 𝐴 = ∅ → ( 𝐴 ≈ ∅ ↔ ∅ ≈ ∅ ) )
11 9 10 mpbiri ( 𝐴 = ∅ → 𝐴 ≈ ∅ )
12 7 11 impbii ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )