Metamath Proof Explorer


Theorem 0nelopabOLD

Description: Obsolete version of 0nelopab as of 3-Oct-2024. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 0nelopabOLD ¬ x y | φ

Proof

Step Hyp Ref Expression
1 elopab x y | φ x y = x y φ
2 nfopab1 _ x x y | φ
3 2 nfel2 x x y | φ
4 3 nfn x ¬ x y | φ
5 nfopab2 _ y x y | φ
6 5 nfel2 y x y | φ
7 6 nfn y ¬ x y | φ
8 vex x V
9 vex y V
10 8 9 opnzi x y
11 nesym x y ¬ = x y
12 pm2.21 ¬ = x y = x y ¬ x y | φ
13 11 12 sylbi x y = x y ¬ x y | φ
14 10 13 ax-mp = x y ¬ x y | φ
15 14 adantr = x y φ ¬ x y | φ
16 7 15 exlimi y = x y φ ¬ x y | φ
17 4 16 exlimi x y = x y φ ¬ x y | φ
18 1 17 sylbi x y | φ ¬ x y | φ
19 id ¬ x y | φ ¬ x y | φ
20 18 19 pm2.61i ¬ x y | φ