Metamath Proof Explorer

Theorem noel

Description: The empty set has no elements. Theorem 6.14 of Quine p. 44. (Contributed by NM, 21-Jun-1993) (Proof shortened by Mario Carneiro, 1-Sep-2015) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

Ref Expression
Assertion noel ⊢ ¬ A ∈ ∅

Proof

Step Hyp Ref Expression
1 pm3.24 ⊢ ¬ y ∈ V ∧ ¬ y ∈ V
2 1 nex ⊢ ¬ ∃ y y ∈ V ∧ ¬ y ∈ V
3 df-clab ⊢ x ∈ y | y ∈ V ∧ ¬ y ∈ V ↔ x y y ∈ V ∧ ¬ y ∈ V
4 spsbe ⊢ x y y ∈ V ∧ ¬ y ∈ V → ∃ y y ∈ V ∧ ¬ y ∈ V
5 3 4 sylbi ⊢ x ∈ y | y ∈ V ∧ ¬ y ∈ V → ∃ y y ∈ V ∧ ¬ y ∈ V
6 2 5 mto ⊢ ¬ x ∈ y | y ∈ V ∧ ¬ y ∈ V
7 df-nul ⊢ ∅ = V ∖ V
8 df-dif ⊢ V ∖ V = y | y ∈ V ∧ ¬ y ∈ V
9 7 8 eqtri ⊢ ∅ = y | y ∈ V ∧ ¬ y ∈ V
10 9 eleq2i ⊢ x ∈ ∅ ↔ x ∈ y | y ∈ V ∧ ¬ y ∈ V
11 6 10 mtbir ⊢ ¬ x ∈ ∅
12 11 intnan ⊢ ¬ x = A ∧ x ∈ ∅
13 12 nex ⊢ ¬ ∃ x x = A ∧ x ∈ ∅
14 dfclel ⊢ A ∈ ∅ ↔ ∃ x x = A ∧ x ∈ ∅
15 13 14 mtbir ⊢ ¬ A ∈ ∅