Theorem r1ssel

Description: A set is a subset of the value of the cumulative hierarchy of sets function iff it is an element of the value at the successor. (Contributed by BTernaryTau, 15-Jan-2026)

	Ref	Expression
Assertion	r1ssel	⊢ ( 𝐵 ∈ On → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1suc	⊢ ( 𝐵 ∈ On → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
2	1	eleq2d	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ) )
3		fvex	⊢ ( 𝑅1 ‘ 𝐵 ) ∈ V
4	3	elpw2	⊢ ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
5	2 4	bitr2di	⊢ ( 𝐵 ∈ On → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )