Metamath Proof Explorer

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 \in On \to (A \subseteq R_{1} (B) \leftrightarrow A \in R_{1} (suc B))$

Proof

Step	Hyp	Ref	Expression
1		r1suc	$⊢ B \in On \to R_{1} (suc B) = 𝒫 R_{1} (B)$
2	1	eleq2d	$⊢ B \in On \to (A \in R_{1} (suc B) \leftrightarrow A \in 𝒫 R_{1} (B))$
3		fvex	$⊢ R_{1} (B) \in V$
4	3	elpw2	$⊢ A \in 𝒫 R_{1} (B) \leftrightarrow A \subseteq R_{1} (B)$
5	2 4	bitr2di	$⊢ B \in On \to (A \subseteq R_{1} (B) \leftrightarrow A \in R_{1} (suc B))$