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