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 )