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 \times (B ∖ C) \subseteq A \times B$

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