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

Metamath Proof Explorer

Theorem difxp1ss

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

		Ref	Expression
	Assertion	difxp1ss	$⊢ (A ∖ C) \times B \subseteq A \times B$

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