This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∖ B \subseteq (A ∆ B)$

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