Metamath Proof Explorer

Theorem r1rankid

Description: Any set is a subset of the hierarchy of its rank. (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1rankid 
|- ( A e. V -> A C_ ( R1 ` ( rank ` A ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 unir1 
 |-  U. ( R1 " On ) = _V
3 1 2 eleqtrrdi 
 |-  ( A e. V -> A e. U. ( R1 " On ) )
4 r1rankidb 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
5 3 4 syl 
 |-  ( A e. V -> A C_ ( R1 ` ( rank ` A ) ) )