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