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	⊢ 𝐴 ⊆ suc 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝐴 } )
2		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
3	1 2	sseqtrri	⊢ 𝐴 ⊆ suc 𝐴