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 ) |
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 ) |