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	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
3	1 2	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
4		r1rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
5	3 4	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )