Metamath Proof Explorer


Theorem ab0ALT

Description: Alternate proof of ab0 , shorter but using more axioms. (Contributed by BJ, 19-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ab0ALT x | φ = x ¬ φ

Proof

Step Hyp Ref Expression
1 nfab1 _ x x | φ
2 1 eq0f x | φ = x ¬ x x | φ
3 abid x x | φ φ
4 3 notbii ¬ x x | φ ¬ φ
5 4 albii x ¬ x x | φ x ¬ φ
6 2 5 bitri x | φ = x ¬ φ