Metamath Proof Explorer

Theorem noelOLD

Description: Obsolete version of noel as of 18-Sep-2024. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion noelOLD ⊢ ¬ 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 ∈ ∅