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 e. Tarski /\ A e. T ) -> { A } e. T )

Proof

Step Hyp Ref Expression
1 tskpw
 |-  ( ( T e. Tarski /\ A e. T ) -> ~P A e. T )
2 snsspw
 |-  { A } C_ ~P A
3 tskss
 |-  ( ( T e. Tarski /\ ~P A e. T /\ { A } C_ ~P A ) -> { A } e. T )
4 2 3 mp3an3
 |-  ( ( T e. Tarski /\ ~P A e. T ) -> { A } e. T )
5 1 4 syldan
 |-  ( ( T e. Tarski /\ A e. T ) -> { A } e. T )