Metamath Proof Explorer


Theorem tsksn

Description: A singleton of an element of a Tarski class belongs to the class. JFM CLASSES2 th. 2 (partly). (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 18-Jun-2013)

Ref Expression
Assertion tsksn T Tarski A T A T

Proof

Step Hyp Ref Expression
1 tskpw T Tarski A T 𝒫 A T
2 snsspw A 𝒫 A
3 tskss T Tarski 𝒫 A T A 𝒫 A A T
4 2 3 mp3an3 T Tarski 𝒫 A T A T
5 1 4 syldan T Tarski A T A T