DEF-SDIF. Set Difference ($\mathsf{ZF}$).
The set difference $X\smallsetminus Y$ is the set
\[\{x\in X:x\notin Y\}.\]
PROP-SDIF-EMP.
For any $X$:
- $X\smallsetminus\varnothing=X$.
- $\varnothing\smallsetminus X=\varnothing$.
- $X\smallsetminus X=\varnothing$.
PROP-SDIF-DJ.
If $X$ and $Y$ are disjoint, then $X\smallsetminus Y=X$ and $Y\smallsetminus X=Y$.
PROP-SDIF-SUB.
If $X\subseteq Y$, then $X\smallsetminus Y=\varnothing$.