Metamath Proof Explorer


Theorem ranksn

Description: The rank of a singleton. Theorem 15.17(v) of Monk1 p. 112. (Contributed by NM, 28-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypothesis ranksn.1 A V
Assertion ranksn rank A = suc rank A

Proof

Step Hyp Ref Expression
1 ranksn.1 A V
2 unir1 R1 On = V
3 1 2 eleqtrri A R1 On
4 ranksnb A R1 On rank A = suc rank A
5 3 4 ax-mp rank A = suc rank A