Description: Alternate definition of the empty set. Definition 5.14 of TakeutiZaring p. 20. (Contributed by NM, 26-Dec-1996) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)
|- (/) = { x | -. x = x }
|- (/) = ( _V \ _V )
|- ( _V \ _V ) = { x | ( x e. _V /\ -. x e. _V ) }
|- -. ( x e. _V /\ -. x e. _V )
|- x = x
|- -. -. x = x
|- ( ( x e. _V /\ -. x e. _V ) <-> -. x = x )
|- { x | ( x e. _V /\ -. x e. _V ) } = { x | -. x = x }