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 e. A | -. x e. A }

Proof

Step Hyp Ref Expression
1 fal 
 |-  -. F.
2 pm3.24 
 |-  -. ( x e. A /\ -. x e. A )
3 1 2 2false 
 |-  ( F. <-> ( x e. A /\ -. x e. A ) )
4 3 abbii 
 |-  { x | F. } = { x | ( x e. A /\ -. x e. A ) }
5 dfnul4 
 |-  (/) = { x | F. }
6 df-rab 
 |-  { x e. A | -. x e. A } = { x | ( x e. A /\ -. x e. A ) }
7 4 5 6 3eqtr4i 
 |-  (/) = { x e. A | -. x e. A }