Metamath Proof Explorer

Theorem indifdi

Description: Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024)

		Ref	Expression
	Assertion	indifdi	$⊢ A \cap (B ∖ C) = (A \cap B) ∖ (A \cap C)$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (A \cap (B ∖ C)) \leftrightarrow (x \in A \land x \in (B ∖ C))$
2		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
3	2	anbi2i	$⊢ (x \in A \land x \in (B ∖ C)) \leftrightarrow (x \in A \land (x \in B \land \neg x \in C))$
4		abai	$⊢ (x \in A \land \neg x \in C) \leftrightarrow (x \in A \land (x \in A \to \neg x \in C))$
5	4	anbi2i	$⊢ (x \in B \land (x \in A \land \neg x \in C)) \leftrightarrow (x \in B \land (x \in A \land (x \in A \to \neg x \in C)))$
6		an12	$⊢ (x \in A \land (x \in B \land \neg x \in C)) \leftrightarrow (x \in B \land (x \in A \land \neg x \in C))$
7		eldif	$⊢ x \in ((A \cap B) ∖ (A \cap C)) \leftrightarrow (x \in (A \cap B) \land \neg x \in (A \cap C))$
8		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
9	8	bicomi	$⊢ (x \in A \land x \in B) \leftrightarrow x \in (A \cap B)$
10		imnan	$⊢ (x \in A \to \neg x \in C) \leftrightarrow \neg (x \in A \land x \in C)$
11		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
12	10 11	xchbinxr	$⊢ (x \in A \to \neg x \in C) \leftrightarrow \neg x \in (A \cap C)$
13	9 12	anbi12i	$⊢ ((x \in A \land x \in B) \land (x \in A \to \neg x \in C)) \leftrightarrow (x \in (A \cap B) \land \neg x \in (A \cap C))$
14		an21	$⊢ ((x \in A \land x \in B) \land (x \in A \to \neg x \in C)) \leftrightarrow (x \in B \land (x \in A \land (x \in A \to \neg x \in C)))$
15	7 13 14	3bitr2i	$⊢ x \in ((A \cap B) ∖ (A \cap C)) \leftrightarrow (x \in B \land (x \in A \land (x \in A \to \neg x \in C)))$
16	5 6 15	3bitr4i	$⊢ (x \in A \land (x \in B \land \neg x \in C)) \leftrightarrow x \in ((A \cap B) ∖ (A \cap C))$
17	1 3 16	3bitri	$⊢ x \in (A \cap (B ∖ C)) \leftrightarrow x \in ((A \cap B) ∖ (A \cap C))$
18	17	eqriv	$⊢ A \cap (B ∖ C) = (A \cap B) ∖ (A \cap C)$