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	|- ( B e. On -> ( A C_ ( R1 ` B ) <-> A e. ( R1 ` suc B ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1suc	|- ( B e. On -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
2	1	eleq2d	|- ( B e. On -> ( A e. ( R1 ` suc B ) <-> A e. ~P ( R1 ` B ) ) )
3		fvex	|- ( R1 ` B ) e. _V
4	3	elpw2	|- ( A e. ~P ( R1 ` B ) <-> A C_ ( R1 ` B ) )
5	2 4	bitr2di	|- ( B e. On -> ( A C_ ( R1 ` B ) <-> A e. ( R1 ` suc B ) ) )