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 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dftr3	⊢ ( Tr 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 )
2		sseq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3	2	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )
4	1 3	sylbi	⊢ ( Tr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )