Metamath Proof Explorer


Theorem ab0OLD

Description: Obsolete version of ab0 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ab0OLD x | φ = x ¬ φ

Proof

Step Hyp Ref Expression
1 dfnul4 = x |
2 1 eqeq2i x | φ = x | φ = x |
3 dfcleq x | φ = x | y y x | φ y x |
4 df-clab y x | φ y x φ
5 sb6 y x φ x x = y φ
6 4 5 bitri y x | φ x x = y φ
7 df-clab y x | y x
8 sbv y x
9 7 8 bitri y x |
10 6 9 bibi12i y x | φ y x | x x = y φ
11 10 albii y y x | φ y x | y x x = y φ
12 nbfal ¬ x x = y φ x x = y φ
13 12 bicomi x x = y φ ¬ x x = y φ
14 13 albii y x x = y φ y ¬ x x = y φ
15 nfna1 x ¬ x x = y φ
16 nfv y ¬ φ
17 pm2.27 x = y x = y φ φ
18 17 spsd x = y x x = y φ φ
19 18 equcoms y = x x x = y φ φ
20 ax12v x = y φ x x = y φ
21 20 equcoms y = x φ x x = y φ
22 19 21 impbid y = x x x = y φ φ
23 22 notbid y = x ¬ x x = y φ ¬ φ
24 15 16 23 cbvalv1 y ¬ x x = y φ x ¬ φ
25 11 14 24 3bitri y y x | φ y x | x ¬ φ
26 2 3 25 3bitri x | φ = x ¬ φ