difxp2

Description: Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013) (Revised by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	difxp2	$⊢ A \times (B ∖ C) = (A \times B) ∖ (A \times C)$

Step	Hyp	Ref	Expression
1		difxp	$⊢ (A \times B) ∖ (A \times C) = ((A ∖ A) \times B) \cup (A \times (B ∖ C))$
2		difid	$⊢ A ∖ A = \emptyset$
3	2	xpeq1i	$⊢ (A ∖ A) \times B = \emptyset \times B$
4		0xp	$⊢ \emptyset \times B = \emptyset$
5	3 4	eqtri	$⊢ (A ∖ A) \times B = \emptyset$
6	5	uneq1i	$⊢ ((A ∖ A) \times B) \cup (A \times (B ∖ C)) = \emptyset \cup (A \times (B ∖ C))$
7		uncom	$⊢ \emptyset \cup (A \times (B ∖ C)) = (A \times (B ∖ C)) \cup \emptyset$
8		un0	$⊢ (A \times (B ∖ C)) \cup \emptyset = A \times (B ∖ C)$
9	7 8	eqtri	$⊢ \emptyset \cup (A \times (B ∖ C)) = A \times (B ∖ C)$
10	1 6 9	3eqtrri	$⊢ A \times (B ∖ C) = (A \times B) ∖ (A \times C)$

Metamath Proof Explorer