Theorem sucssel

Description: A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995)

	Ref	Expression
Assertion	sucssel	$$⊢A\in V\to \left(\mathrm{suc}A\subseteq B\to A\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sucidg	$$⊢A\in V\to A\in \mathrm{suc}A$$
2		ssel	$$⊢\mathrm{suc}A\subseteq B\to \left(A\in \mathrm{suc}A\to A\in B\right)$$
3	1 2	syl5com	$$⊢A\in V\to \left(\mathrm{suc}A\subseteq B\to A\in B\right)$$