This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cardeq0

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

Ref Expression
Assertion cardeq0 ⊢ A ∈ V → card ⁡ A = ∅ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 carden ⊢ A ∈ V ∧ ∅ ∈ V → card ⁡ A = card ⁡ ∅ ↔ A ≈ ∅
3 1 2 mpan2 ⊢ A ∈ V → card ⁡ A = card ⁡ ∅ ↔ A ≈ ∅
4 card0 ⊢ card ⁡ ∅ = ∅
5 4 eqeq2i ⊢ card ⁡ A = card ⁡ ∅ ↔ card ⁡ A = ∅
6 en0 ⊢ A ≈ ∅ ↔ A = ∅
7 3 5 6 3bitr3g ⊢ A ∈ V → card ⁡ A = ∅ ↔ A = ∅