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 
 |-  (/) e. _V
3 hasheq0 
 |-  ( (/) e. _V -> ( ( # ` (/) ) = 0 <-> (/) = (/) ) )
4 2 3 ax-mp 
 |-  ( ( # ` (/) ) = 0 <-> (/) = (/) )
5 1 4 mpbir 
 |-  ( # ` (/) ) = 0