Metamath Proof Explorer


Theorem cardeq0

Description: Only the empty set has cardinality zero. (Contributed by NM, 23-Apr-2004)

Ref Expression
Assertion cardeq0 ( 𝐴𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 carden ( ( 𝐴𝑉 ∧ ∅ ∈ V ) → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
3 1 2 mpan2 ( 𝐴𝑉 → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
4 card0 ( card ‘ ∅ ) = ∅
5 4 eqeq2i ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ ( card ‘ 𝐴 ) = ∅ )
6 en0 ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
7 3 5 6 3bitr3g ( 𝐴𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )