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	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ ( 𝐴 △ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
2		df-symdif	⊢ ( 𝐴 △ 𝐵 ) = ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) )
3	1 2	sseqtrri	⊢ ( 𝐴 ∖ 𝐵 ) ⊆ ( 𝐴 △ 𝐵 )