difxp

Description: Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 26-Jun-2014) (Proof shortened by Wolf Lammen, 16-May-2025)

		Ref	Expression
	Assertion	difxp	$⊢ (C \times D) ∖ (A \times B) = ((C ∖ A) \times D) \cup (C \times (D ∖ B))$

Proof

Step	Hyp	Ref	Expression
1		difss	$⊢ (C \times D) ∖ (A \times B) \subseteq C \times D$
2		relxp	$⊢ Rel (C \times D)$
3		relss	$⊢ (C \times D) ∖ (A \times B) \subseteq C \times D \to (Rel (C \times D) \to Rel ((C \times D) ∖ (A \times B)))$
4	1 2 3	mp2	$⊢ Rel ((C \times D) ∖ (A \times B))$
5		relxp	$⊢ Rel ((C ∖ A) \times D)$
6		relxp	$⊢ Rel (C \times (D ∖ B))$
7		relun	$⊢ Rel (((C ∖ A) \times D) \cup (C \times (D ∖ B))) \leftrightarrow (Rel ((C ∖ A) \times D) \land Rel (C \times (D ∖ B)))$
8	5 6 7	mpbir2an	$⊢ Rel (((C ∖ A) \times D) \cup (C \times (D ∖ B)))$
9		ianor	$⊢ \neg (x \in A \land y \in B) \leftrightarrow (\neg x \in A \lor \neg y \in B)$
10	9	anbi2i	$⊢ ((x \in C \land y \in D) \land \neg (x \in A \land y \in B)) \leftrightarrow ((x \in C \land y \in D) \land (\neg x \in A \lor \neg y \in B))$
11		andi	$⊢ ((x \in C \land y \in D) \land (\neg x \in A \lor \neg y \in B)) \leftrightarrow (((x \in C \land y \in D) \land \neg x \in A) \lor ((x \in C \land y \in D) \land \neg y \in B))$
12	10 11	bitri	$⊢ ((x \in C \land y \in D) \land \neg (x \in A \land y \in B)) \leftrightarrow (((x \in C \land y \in D) \land \neg x \in A) \lor ((x \in C \land y \in D) \land \neg y \in B))$
13		opelxp	$⊢ ⟨x, y⟩ \in (C \times D) \leftrightarrow (x \in C \land y \in D)$
14		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
15	14	notbii	$⊢ \neg ⟨x, y⟩ \in (A \times B) \leftrightarrow \neg (x \in A \land y \in B)$
16	13 15	anbi12i	$⊢ (⟨x, y⟩ \in (C \times D) \land \neg ⟨x, y⟩ \in (A \times B)) \leftrightarrow ((x \in C \land y \in D) \land \neg (x \in A \land y \in B))$
17		opelxp	$⊢ ⟨x, y⟩ \in ((C ∖ A) \times D) \leftrightarrow (x \in (C ∖ A) \land y \in D)$
18		eldif	$⊢ x \in (C ∖ A) \leftrightarrow (x \in C \land \neg x \in A)$
19	18	anbi1i	$⊢ (x \in (C ∖ A) \land y \in D) \leftrightarrow ((x \in C \land \neg x \in A) \land y \in D)$
20		an32	$⊢ ((x \in C \land \neg x \in A) \land y \in D) \leftrightarrow ((x \in C \land y \in D) \land \neg x \in A)$
21	17 19 20	3bitri	$⊢ ⟨x, y⟩ \in ((C ∖ A) \times D) \leftrightarrow ((x \in C \land y \in D) \land \neg x \in A)$
22		eldif	$⊢ y \in (D ∖ B) \leftrightarrow (y \in D \land \neg y \in B)$
23	22	anbi2i	$⊢ (x \in C \land y \in (D ∖ B)) \leftrightarrow (x \in C \land (y \in D \land \neg y \in B))$
24		opelxp	$⊢ ⟨x, y⟩ \in (C \times (D ∖ B)) \leftrightarrow (x \in C \land y \in (D ∖ B))$
25		anass	$⊢ ((x \in C \land y \in D) \land \neg y \in B) \leftrightarrow (x \in C \land (y \in D \land \neg y \in B))$
26	23 24 25	3bitr4i	$⊢ ⟨x, y⟩ \in (C \times (D ∖ B)) \leftrightarrow ((x \in C \land y \in D) \land \neg y \in B)$
27	21 26	orbi12i	$⊢ (⟨x, y⟩ \in ((C ∖ A) \times D) \lor ⟨x, y⟩ \in (C \times (D ∖ B))) \leftrightarrow (((x \in C \land y \in D) \land \neg x \in A) \lor ((x \in C \land y \in D) \land \neg y \in B))$
28	12 16 27	3bitr4i	$⊢ (⟨x, y⟩ \in (C \times D) \land \neg ⟨x, y⟩ \in (A \times B)) \leftrightarrow (⟨x, y⟩ \in ((C ∖ A) \times D) \lor ⟨x, y⟩ \in (C \times (D ∖ B)))$
29		eldif	$⊢ ⟨x, y⟩ \in ((C \times D) ∖ (A \times B)) \leftrightarrow (⟨x, y⟩ \in (C \times D) \land \neg ⟨x, y⟩ \in (A \times B))$
30		elun	$⊢ ⟨x, y⟩ \in (((C ∖ A) \times D) \cup (C \times (D ∖ B))) \leftrightarrow (⟨x, y⟩ \in ((C ∖ A) \times D) \lor ⟨x, y⟩ \in (C \times (D ∖ B)))$
31	28 29 30	3bitr4i	$⊢ ⟨x, y⟩ \in ((C \times D) ∖ (A \times B)) \leftrightarrow ⟨x, y⟩ \in (((C ∖ A) \times D) \cup (C \times (D ∖ B)))$
32	4 8 31	eqrelriiv	$⊢ (C \times D) ∖ (A \times B) = ((C ∖ A) \times D) \cup (C \times (D ∖ B))$

Metamath Proof Explorer

Theorem difxp

Proof