Theorem sssucid

Description: A class is included in its own successor. Part of Proposition 7.23 of TakeutiZaring p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994)

	Ref	Expression
Assertion	sssucid	$$⊢A\subseteq \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup \left\{A\right\}$$
2		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
3	1 2	sseqtrri	$$⊢A\subseteq \mathrm{suc}A$$