Description: The rank of the empty set is (/) . (Contributed by Scott Fenton, 17-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | rank0 | ⊢ ( rank ‘ ∅ ) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ∅ = ∅ | |
2 | 0ex | ⊢ ∅ ∈ V | |
3 | 2 | rankeq0 | ⊢ ( ∅ = ∅ ↔ ( rank ‘ ∅ ) = ∅ ) |
4 | 1 3 | mpbi | ⊢ ( rank ‘ ∅ ) = ∅ |