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 ) C_ ( A /_\ B )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  ( A \ B ) C_ ( ( A \ B ) u. ( B \ A ) )
2 df-symdif 
 |-  ( A /_\ B ) = ( ( A \ B ) u. ( B \ A ) )
3 1 2 sseqtrri 
 |-  ( A \ B ) C_ ( A /_\ B )