Theorem trss

Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994) (Proof shortened by JJ, 26-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dftr3	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\in Ax\subseteq A$$
2		sseq1	$$⊢x=B\to \left(x\subseteq A\leftrightarrow B\subseteq A\right)$$
3	2	rspccv	$$⊢\forall x\in Ax\subseteq A\to \left(B\in A\to B\subseteq A\right)$$
4	1 3	sylbi	$$⊢\mathrm{Tr}A\to \left(B\in A\to B\subseteq A\right)$$