This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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