|Description: Define class difference,
also called relative complement. Definition
5.12 of [TakeutiZaring] p. 20.
(ex-dif 20810). Contrast this
operation with union (df-un 3157) and intersection
(df-in 3159). Several notations are used in the
literature; we chose the convention used in Definition 5.3 of
[Eisenberg] p. 67 instead of the more
common minus sign to reserve the
latter for later use in, e.g., arithmetic. We will use the
terminology " excludes
" to mean . We will
use " is
removed from "
removal of an element or equivalently the exclusion of a singleton.
(Contributed by NM, 29-Apr-1994.)|