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

Metamath Proof Explorer

Theorem difsymssdifssd

Description: If the symmetric difference is contained in C , so is one of the differences. (Contributed by AV, 17-Aug-2022)

		Ref	Expression
	Hypothesis	difsymssdifssd.1	$⊢ φ \to (A ∆ B) \subseteq C$
	Assertion	difsymssdifssd	$⊢ φ \to A ∖ B \subseteq C$

Step	Hyp	Ref	Expression
1		difsymssdifssd.1	$⊢ φ \to (A ∆ B) \subseteq C$
2		difsssymdif	$⊢ A ∖ B \subseteq (A ∆ B)$
3	2 1	sstrid	$⊢ φ \to A ∖ B \subseteq C$