Metamath Proof Explorer


Theorem tsk0

Description: A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 18-Jun-2013)

Ref Expression
Assertion tsk0
|- ( ( T e. Tarski /\ T =/= (/) ) -> (/) e. T )

Proof

Step Hyp Ref Expression
1 n0
 |-  ( T =/= (/) <-> E. x x e. T )
2 0ss
 |-  (/) C_ x
3 tskss
 |-  ( ( T e. Tarski /\ x e. T /\ (/) C_ x ) -> (/) e. T )
4 2 3 mp3an3
 |-  ( ( T e. Tarski /\ x e. T ) -> (/) e. T )
5 4 expcom
 |-  ( x e. T -> ( T e. Tarski -> (/) e. T ) )
6 5 exlimiv
 |-  ( E. x x e. T -> ( T e. Tarski -> (/) e. T ) )
7 1 6 sylbi
 |-  ( T =/= (/) -> ( T e. Tarski -> (/) e. T ) )
8 7 impcom
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> (/) e. T )