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 ⊢ ( 𝜑 → ( 𝐴 △ 𝐵 ) ⊆ 𝐶 )
Assertion difsymssdifssd ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 difsymssdifssd.1 ⊢ ( 𝜑 → ( 𝐴 △ 𝐵 ) ⊆ 𝐶 )
2 difsssymdif ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ ( 𝐴 △ 𝐵 )
3 2 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐶 )