Metamath Proof Explorer


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 Tarski A T B A B T

Proof

Step Hyp Ref Expression
1 elpw2g A T B 𝒫 A B A
2 1 adantl T Tarski A T B 𝒫 A B A
3 tskpwss T Tarski A T 𝒫 A T
4 3 sseld T Tarski A T B 𝒫 A B T
5 2 4 sylbird T Tarski A T B A B T
6 5 3impia T Tarski A T B A B T