Theorem difxp1ss

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

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

Proof

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