Metamath Proof Explorer


Theorem difxp2ss

Description: Difference law for Cartesian products. (Contributed by Thierry Arnoux, 24-Jul-2023)

Ref Expression
Assertion difxp2ss
|- ( A X. ( B \ C ) ) C_ ( A X. B )

Proof

Step Hyp Ref Expression
1 difxp2
 |-  ( A X. ( B \ C ) ) = ( ( A X. B ) \ ( A X. C ) )
2 difss
 |-  ( ( A X. B ) \ ( A X. C ) ) C_ ( A X. B )
3 1 2 eqsstri
 |-  ( A X. ( B \ C ) ) C_ ( A X. B )