Theorem trsucss

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

	Ref	Expression
Assertion	trsucss	⊢ ( Tr 𝐴 → ( 𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elsuci	⊢ ( 𝐵 ∈ suc 𝐴 → ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) )
2		trss	⊢ ( Tr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) )
3		eqimss	⊢ ( 𝐵 = 𝐴 → 𝐵 ⊆ 𝐴 )
4	3	a1i	⊢ ( Tr 𝐴 → ( 𝐵 = 𝐴 → 𝐵 ⊆ 𝐴 ) )
5	2 4	jaod	⊢ ( Tr 𝐴 → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) → 𝐵 ⊆ 𝐴 ) )
6	1 5	syl5	⊢ ( Tr 𝐴 → ( 𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴 ) )