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 )