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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∅ ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝑇 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑇 )
2		0ss	⊢ ∅ ⊆ 𝑥
3		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ ∅ ⊆ 𝑥 ) → ∅ ∈ 𝑇 )
4	2 3	mp3an3	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → ∅ ∈ 𝑇 )
5	4	expcom	⊢ ( 𝑥 ∈ 𝑇 → ( 𝑇 ∈ Tarski → ∅ ∈ 𝑇 ) )
6	5	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ 𝑇 → ( 𝑇 ∈ Tarski → ∅ ∈ 𝑇 ) )
7	1 6	sylbi	⊢ ( 𝑇 ≠ ∅ → ( 𝑇 ∈ Tarski → ∅ ∈ 𝑇 ) )
8	7	impcom	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∅ ∈ 𝑇 )