Theorem tsktrss

Description: A transitive element of a Tarski class is a part of the class. JFM CLASSES2 th. 8. (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tsktrss	|- ( ( T e. Tarski /\ Tr A /\ A e. T ) -> A C_ T )

Proof

Step	Hyp	Ref	Expression
1		simp2	|- ( ( T e. Tarski /\ Tr A /\ A e. T ) -> Tr A )
2		dftr4	|- ( Tr A <-> A C_ ~P A )
3	1 2	sylib	|- ( ( T e. Tarski /\ Tr A /\ A e. T ) -> A C_ ~P A )
4		tskpwss	|- ( ( T e. Tarski /\ A e. T ) -> ~P A C_ T )
5	4	3adant2	|- ( ( T e. Tarski /\ Tr A /\ A e. T ) -> ~P A C_ T )
6	3 5	sstrd	|- ( ( T e. Tarski /\ Tr A /\ A e. T ) -> A C_ T )