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 A -> ( B e. suc A -> B C_ A ) )

Proof

Step	Hyp	Ref	Expression
1		elsuci	|- ( B e. suc A -> ( B e. A \/ B = A ) )
2		trss	|- ( Tr A -> ( B e. A -> B C_ A ) )
3		eqimss	|- ( B = A -> B C_ A )
4	3	a1i	|- ( Tr A -> ( B = A -> B C_ A ) )
5	2 4	jaod	|- ( Tr A -> ( ( B e. A \/ B = A ) -> B C_ A ) )
6	1 5	syl5	|- ( Tr A -> ( B e. suc A -> B C_ A ) )