Set Difference

DEF-SD. Set Difference.

The set difference between $X$ and $Y$ is

\[X\setminus Y = \{x\in X:x\notin Y\}.\]

PROP-SD-EMP.

For any $X$:

1. \[X\smallsetminus\varnothing = X.\]
2. \[\varnothing\smallsetminus X = \varnothing.\]
3. \[X\smallsetminus X = \varnothing.\]

PROP-SD-DJ.

If $X$ and $Y$ are disjoint, then $X\smallsetminus Y=X$ and $Y\smallsetminus X=Y$.

PROP-SD-SUB.

If $X\subseteq Y$, then $X\smallsetminus Y=\varnothing$.