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 
 |-  (/) e. On
2 cardonle 
 |-  ( (/) e. On -> ( card ` (/) ) C_ (/) )
3 1 2 ax-mp 
 |-  ( card ` (/) ) C_ (/)
4 ss0b 
 |-  ( ( card ` (/) ) C_ (/) <-> ( card ` (/) ) = (/) )
5 3 4 mpbi 
 |-  ( card ` (/) ) = (/)