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