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

Metamath Proof Explorer

Theorem undif4

Description: Distribute union over difference. (Contributed by NM, 17-May-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	undif4	$⊢ A \cap C = \emptyset \to A \cup (B ∖ C) = (A \cup B) ∖ C$

Proof

Step	Hyp	Ref	Expression
1		pm2.621	$⊢ (x \in A \to \neg x \in C) \to ((x \in A \lor \neg x \in C) \to \neg x \in C)$
2		olc	$⊢ \neg x \in C \to (x \in A \lor \neg x \in C)$
3	1 2	impbid1	$⊢ (x \in A \to \neg x \in C) \to ((x \in A \lor \neg x \in C) \leftrightarrow \neg x \in C)$
4	3	anbi2d	$⊢ (x \in A \to \neg x \in C) \to (((x \in A \lor x \in B) \land (x \in A \lor \neg x \in C)) \leftrightarrow ((x \in A \lor x \in B) \land \neg x \in C))$
5		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
6	5	orbi2i	$⊢ (x \in A \lor x \in (B ∖ C)) \leftrightarrow (x \in A \lor (x \in B \land \neg x \in C))$
7		ordi	$⊢ (x \in A \lor (x \in B \land \neg x \in C)) \leftrightarrow ((x \in A \lor x \in B) \land (x \in A \lor \neg x \in C))$
8	6 7	bitri	$⊢ (x \in A \lor x \in (B ∖ C)) \leftrightarrow ((x \in A \lor x \in B) \land (x \in A \lor \neg x \in C))$
9		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
10	9	anbi1i	$⊢ (x \in (A \cup B) \land \neg x \in C) \leftrightarrow ((x \in A \lor x \in B) \land \neg x \in C)$
11	4 8 10	3bitr4g	$⊢ (x \in A \to \neg x \in C) \to ((x \in A \lor x \in (B ∖ C)) \leftrightarrow (x \in (A \cup B) \land \neg x \in C))$
12		elun	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow (x \in A \lor x \in (B ∖ C))$
13		eldif	$⊢ x \in ((A \cup B) ∖ C) \leftrightarrow (x \in (A \cup B) \land \neg x \in C)$
14	11 12 13	3bitr4g	$⊢ (x \in A \to \neg x \in C) \to (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ C))$
15	14	alimi	$⊢ \forall x (x \in A \to \neg x \in C) \to \forall x (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ C))$
16		disj1	$⊢ A \cap C = \emptyset \leftrightarrow \forall x (x \in A \to \neg x \in C)$
17		dfcleq	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ C \leftrightarrow \forall x (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ C))$
18	15 16 17	3imtr4i	$⊢ A \cap C = \emptyset \to A \cup (B ∖ C) = (A \cup B) ∖ C$