This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )