Theorem difxp2ss

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

	Ref	Expression
Assertion	difxp2ss	$$⊢A\times \left(B\setminus C\right)\subseteq A\times B$$

Proof

Step	Hyp	Ref	Expression
1		difxp2	$$⊢A\times \left(B\setminus C\right)=\left(A\times B\right)\setminus \left(A\times C\right)$$
2		difss	$$⊢\left(A\times B\right)\setminus \left(A\times C\right)\subseteq A\times B$$
3	1 2	eqsstri	$$⊢A\times \left(B\setminus C\right)\subseteq A\times B$$