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 C_ suc A

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- A C_ ( A u. { A } )
2		df-suc	|- suc A = ( A u. { A } )
3	1 2	sseqtrri	|- A C_ suc A