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 \in Tarski \land T \neq \emptyset) \to \emptyset \in T$

Step	Hyp	Ref	Expression
1		n0	$⊢ T \neq \emptyset \leftrightarrow \exists x x \in T$
2		0ss	$⊢ \emptyset \subseteq x$
3		tskss	$⊢ (T \in Tarski \land x \in T \land \emptyset \subseteq x) \to \emptyset \in T$
4	2 3	mp3an3	$⊢ (T \in Tarski \land x \in T) \to \emptyset \in T$
5	4	expcom	$⊢ x \in T \to (T \in Tarski \to \emptyset \in T)$
6	5	exlimiv	$⊢ \exists x x \in T \to (T \in Tarski \to \emptyset \in T)$
7	1 6	sylbi	$⊢ T \neq \emptyset \to (T \in Tarski \to \emptyset \in T)$
8	7	impcom	$⊢ (T \in Tarski \land T \neq \emptyset) \to \emptyset \in T$

Metamath Proof Explorer