Metamath Proof Explorer


Theorem tskpwss

Description: First axiom of a Tarski class. The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tskpwss T Tarski A T 𝒫 A T

Proof

Step Hyp Ref Expression
1 eltskg T Tarski T Tarski x T 𝒫 x T y T 𝒫 x y x 𝒫 T x T x T
2 1 ibi T Tarski x T 𝒫 x T y T 𝒫 x y x 𝒫 T x T x T
3 2 simpld T Tarski x T 𝒫 x T y T 𝒫 x y
4 simpl 𝒫 x T y T 𝒫 x y 𝒫 x T
5 4 ralimi x T 𝒫 x T y T 𝒫 x y x T 𝒫 x T
6 3 5 syl T Tarski x T 𝒫 x T
7 pweq x = A 𝒫 x = 𝒫 A
8 7 sseq1d x = A 𝒫 x T 𝒫 A T
9 8 rspccva x T 𝒫 x T A T 𝒫 A T
10 6 9 sylan T Tarski A T 𝒫 A T