Metamath Proof Explorer

Theorem ranksng

Description: The rank of a singleton. Closed form of ranksn . (Contributed by Scott Fenton, 15-Jul-2015)

Ref Expression
Assertion ranksng 
|- ( A e. V -> ( rank ` { A } ) = suc ( rank ` A ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = A -> { x } = { A } )
2 1 fveq2d 
 |-  ( x = A -> ( rank ` { x } ) = ( rank ` { A } ) )
3 fveq2 
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
4 suceq 
 |-  ( ( rank ` x ) = ( rank ` A ) -> suc ( rank ` x ) = suc ( rank ` A ) )
5 3 4 syl 
 |-  ( x = A -> suc ( rank ` x ) = suc ( rank ` A ) )
6 2 5 eqeq12d 
 |-  ( x = A -> ( ( rank ` { x } ) = suc ( rank ` x ) <-> ( rank ` { A } ) = suc ( rank ` A ) ) )
7 vex 
 |-  x e. _V
8 7 ranksn 
 |-  ( rank ` { x } ) = suc ( rank ` x )
9 6 8 vtoclg 
 |-  ( A e. V -> ( rank ` { A } ) = suc ( rank ` A ) )