# 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 ${⊢}\left({T}\in \mathrm{Tarski}\wedge {T}\ne \varnothing \right)\to \varnothing \in {T}$

### Proof

Step Hyp Ref Expression
1 n0 ${⊢}{T}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {T}$
2 0ss ${⊢}\varnothing \subseteq {x}$
3 tskss ${⊢}\left({T}\in \mathrm{Tarski}\wedge {x}\in {T}\wedge \varnothing \subseteq {x}\right)\to \varnothing \in {T}$
4 2 3 mp3an3 ${⊢}\left({T}\in \mathrm{Tarski}\wedge {x}\in {T}\right)\to \varnothing \in {T}$
5 4 expcom ${⊢}{x}\in {T}\to \left({T}\in \mathrm{Tarski}\to \varnothing \in {T}\right)$
6 5 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {T}\to \left({T}\in \mathrm{Tarski}\to \varnothing \in {T}\right)$
7 1 6 sylbi ${⊢}{T}\ne \varnothing \to \left({T}\in \mathrm{Tarski}\to \varnothing \in {T}\right)$
8 7 impcom ${⊢}\left({T}\in \mathrm{Tarski}\wedge {T}\ne \varnothing \right)\to \varnothing \in {T}$