Theorem difsssymdif

Description: The symmetric difference contains one of the differences. (Proposed by BJ, 18-Aug-2022.) (Contributed by AV, 19-Aug-2022)

	Ref	Expression
Assertion	difsssymdif	$$⊢A\setminus B\subseteq \left(A∆B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\setminus B\subseteq \left(A\setminus B\right)\cup \left(B\setminus A\right)$$
2		df-symdif	$$⊢\left(A∆B\right)=\left(A\setminus B\right)\cup \left(B\setminus A\right)$$
3	1 2	sseqtrri	$$⊢A\setminus B\subseteq \left(A∆B\right)$$