Metamath Proof Explorer


Theorem hash0

Description: The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014)

Ref Expression
Assertion hash0 ( ♯ ‘ ∅ ) = 0

Proof

Step Hyp Ref Expression
1 eqid ∅ = ∅
2 0ex ∅ ∈ V
3 hasheq0 ( ∅ ∈ V → ( ( ♯ ‘ ∅ ) = 0 ↔ ∅ = ∅ ) )
4 2 3 ax-mp ( ( ♯ ‘ ∅ ) = 0 ↔ ∅ = ∅ )
5 1 4 mpbir ( ♯ ‘ ∅ ) = 0