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