Theorem tskss

Description: The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 18-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		elpw2g	|- ( A e. T -> ( B e. ~P A <-> B C_ A ) )
2	1	adantl	|- ( ( T e. Tarski /\ A e. T ) -> ( B e. ~P A <-> B C_ A ) )
3		tskpwss	|- ( ( T e. Tarski /\ A e. T ) -> ~P A C_ T )
4	3	sseld	|- ( ( T e. Tarski /\ A e. T ) -> ( B e. ~P A -> B e. T ) )
5	2 4	sylbird	|- ( ( T e. Tarski /\ A e. T ) -> ( B C_ A -> B e. T ) )
6	5	3impia	|- ( ( T e. Tarski /\ A e. T /\ B C_ A ) -> B e. T )