Metamath Proof Explorer

Theorem difxp1ss

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

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

Proof

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