Theorem trsucss

Description: A member of the successor of a transitive class is a subclass of it. Lemma 1.13 of Schloeder p. 2. (Contributed by NM, 4-Oct-2003)

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

Proof

Step	Hyp	Ref	Expression
1		elsuci	$$⊢B\in \mathrm{suc}A\to \left(B\in A\vee B=A\right)$$
2		trss	$$⊢\mathrm{Tr}A\to \left(B\in A\to B\subseteq A\right)$$
3		eqimss	$$⊢B=A\to B\subseteq A$$
4	3	a1i	$$⊢\mathrm{Tr}A\to \left(B=A\to B\subseteq A\right)$$
5	2 4	jaod	$$⊢\mathrm{Tr}A\to \left(\left(B\in A\vee B=A\right)\to B\subseteq A\right)$$
6	1 5	syl5	$$⊢\mathrm{Tr}A\to \left(B\in \mathrm{suc}A\to B\subseteq A\right)$$