indifdirOLD

Description: Obsolete version of indifdir as of 14-Aug-2024. (Contributed by Scott Fenton, 14-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pm3.24	$⊢ \neg (x \in C \land \neg x \in C)$
2	1	intnan	$⊢ \neg (x \in A \land (x \in C \land \neg x \in C))$
3		anass	$⊢ ((x \in A \land x \in C) \land \neg x \in C) \leftrightarrow (x \in A \land (x \in C \land \neg x \in C))$
4	2 3	mtbir	$⊢ \neg ((x \in A \land x \in C) \land \neg x \in C)$
5	4	biorfi	$⊢ ((x \in A \land x \in C) \land \neg x \in B) \leftrightarrow (((x \in A \land x \in C) \land \neg x \in B) \lor ((x \in A \land x \in C) \land \neg x \in C))$
6		an32	$⊢ ((x \in A \land \neg x \in B) \land x \in C) \leftrightarrow ((x \in A \land x \in C) \land \neg x \in B)$
7		andi	$⊢ ((x \in A \land x \in C) \land (\neg x \in B \lor \neg x \in C)) \leftrightarrow (((x \in A \land x \in C) \land \neg x \in B) \lor ((x \in A \land x \in C) \land \neg x \in C))$
8	5 6 7	3bitr4i	$⊢ ((x \in A \land \neg x \in B) \land x \in C) \leftrightarrow ((x \in A \land x \in C) \land (\neg x \in B \lor \neg x \in C))$
9		ianor	$⊢ \neg (x \in B \land x \in C) \leftrightarrow (\neg x \in B \lor \neg x \in C)$
10	9	anbi2i	$⊢ ((x \in A \land x \in C) \land \neg (x \in B \land x \in C)) \leftrightarrow ((x \in A \land x \in C) \land (\neg x \in B \lor \neg x \in C))$
11	8 10	bitr4i	$⊢ ((x \in A \land \neg x \in B) \land x \in C) \leftrightarrow ((x \in A \land x \in C) \land \neg (x \in B \land x \in C))$
12		elin	$⊢ x \in ((A ∖ B) \cap C) \leftrightarrow (x \in (A ∖ B) \land x \in C)$
13		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
14	13	anbi1i	$⊢ (x \in (A ∖ B) \land x \in C) \leftrightarrow ((x \in A \land \neg x \in B) \land x \in C)$
15	12 14	bitri	$⊢ x \in ((A ∖ B) \cap C) \leftrightarrow ((x \in A \land \neg x \in B) \land x \in C)$
16		eldif	$⊢ x \in ((A \cap C) ∖ (B \cap C)) \leftrightarrow (x \in (A \cap C) \land \neg x \in (B \cap C))$
17		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
18		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
19	18	notbii	$⊢ \neg x \in (B \cap C) \leftrightarrow \neg (x \in B \land x \in C)$
20	17 19	anbi12i	$⊢ (x \in (A \cap C) \land \neg x \in (B \cap C)) \leftrightarrow ((x \in A \land x \in C) \land \neg (x \in B \land x \in C))$
21	16 20	bitri	$⊢ x \in ((A \cap C) ∖ (B \cap C)) \leftrightarrow ((x \in A \land x \in C) \land \neg (x \in B \land x \in C))$
22	11 15 21	3bitr4i	$⊢ x \in ((A ∖ B) \cap C) \leftrightarrow x \in ((A \cap C) ∖ (B \cap C))$
23	22	eqriv	$⊢ (A ∖ B) \cap C = (A \cap C) ∖ (B \cap C)$

Metamath Proof Explorer

Theorem indifdirOLD

Proof