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

Metamath Proof Explorer

Theorem card0

Description: The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003)

Ref Expression
Assertion card0 ⊢ card ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 cardonle ⊢ ∅ ∈ On → card ⁡ ∅ ⊆ ∅
3 1 2 ax-mp ⊢ card ⁡ ∅ ⊆ ∅
4 ss0b ⊢ card ⁡ ∅ ⊆ ∅ ↔ card ⁡ ∅ = ∅
5 3 4 mpbi ⊢ card ⁡ ∅ = ∅