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

Metamath Proof Explorer

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	$⊢ Tr A \to (B \in A \to B \subseteq A)$

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