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 ∅ ∈ V
3 2 rankeq0 ( ∅ = ∅ ↔ ( rank ‘ ∅ ) = ∅ )
4 1 3 mpbi ( rank ‘ ∅ ) = ∅