Metamath Proof Explorer


Theorem difxp1ss

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

Ref Expression
Assertion difxp1ss ( ( 𝐴𝐶 ) × 𝐵 ) ⊆ ( 𝐴 × 𝐵 )

Proof

Step Hyp Ref Expression
1 difxp1 ( ( 𝐴𝐶 ) × 𝐵 ) = ( ( 𝐴 × 𝐵 ) ∖ ( 𝐶 × 𝐵 ) )
2 difss ( ( 𝐴 × 𝐵 ) ∖ ( 𝐶 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )
3 1 2 eqsstri ( ( 𝐴𝐶 ) × 𝐵 ) ⊆ ( 𝐴 × 𝐵 )