Metamath Proof Explorer


Theorem dfnul3

Description: Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004) (Proof shortened by BJ, 23-Sep-2024)

Ref Expression
Assertion dfnul3 = x A | ¬ x A

Proof

Step Hyp Ref Expression
1 fal ¬
2 pm3.24 ¬ x A ¬ x A
3 1 2 2false x A ¬ x A
4 3 abbii x | = x | x A ¬ x A
5 dfnul4 = x |
6 df-rab x A | ¬ x A = x | x A ¬ x A
7 4 5 6 3eqtr4i = x A | ¬ x A