Metamath Proof Explorer

Theorem rank0

Description: The rank of the empty set is (/) . (Contributed by Scott Fenton, 17-Jul-2015)

Ref Expression
Assertion rank0 
|- ( rank ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 0ex 
 |-  (/) e. _V
3 2 rankeq0 
 |-  ( (/) = (/) <-> ( rank ` (/) ) = (/) )
4 1 3 mpbi 
 |-  ( rank ` (/) ) = (/)