Metamath Proof Explorer

Theorem dfnul3

Description: Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion dfnul3 
|- (/) = { x e. A | -. x e. A }

Proof

Step Hyp Ref Expression
1 pm3.24 
 |-  -. ( x e. A /\ -. x e. A )
2 equid 
 |-  x = x
3 1 2 2th 
 |-  ( -. ( x e. A /\ -. x e. A ) <-> x = x )
4 3 con1bii 
 |-  ( -. x = x <-> ( x e. A /\ -. x e. A ) )
5 4 abbii 
 |-  { x | -. x = x } = { x | ( x e. A /\ -. x e. A ) }
6 dfnul2 
 |-  (/) = { x | -. x = x }
7 df-rab 
 |-  { x e. A | -. x e. A } = { x | ( x e. A /\ -. x e. A ) }
8 5 6 7 3eqtr4i 
 |-  (/) = { x e. A | -. x e. A }