Metamath Proof Explorer


Theorem dfnul2OLD

Description: Obsolete version of dfnul2 as of 23-Sep-2024. (Contributed by NM, 26-Dec-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfnul2OLD = x | ¬ x = x

Proof

Step Hyp Ref Expression
1 df-nul = V V
2 df-dif V V = x | x V ¬ x V
3 pm3.24 ¬ x V ¬ x V
4 equid x = x
5 4 notnoti ¬ ¬ x = x
6 3 5 2false x V ¬ x V ¬ x = x
7 6 abbii x | x V ¬ x V = x | ¬ x = x
8 1 2 7 3eqtri = x | ¬ x = x