Metamath Proof Explorer

Theorem undif3

Description: An equality involving class union and class difference. The first equality of Exercise 13 of TakeutiZaring p. 22. (Contributed by Alan Sare, 17-Apr-2012) (Proof shortened by JJ, 13-Jul-2021)

		Ref	Expression
	Assertion	undif3	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A)$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
2		pm4.53	$⊢ \neg (x \in C \land \neg x \in A) \leftrightarrow (\neg x \in C \lor x \in A)$
3		eldif	$⊢ x \in (C ∖ A) \leftrightarrow (x \in C \land \neg x \in A)$
4	2 3	xchnxbir	$⊢ \neg x \in (C ∖ A) \leftrightarrow (\neg x \in C \lor x \in A)$
5	1 4	anbi12i	$⊢ (x \in (A \cup B) \land \neg x \in (C ∖ A)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
6		eldif	$⊢ x \in ((A \cup B) ∖ (C ∖ A)) \leftrightarrow (x \in (A \cup B) \land \neg x \in (C ∖ A))$
7		elun	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow (x \in A \lor x \in (B ∖ C))$
8		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
9	8	orbi2i	$⊢ (x \in A \lor x \in (B ∖ C)) \leftrightarrow (x \in A \lor (x \in B \land \neg x \in C))$
10		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))$
11		orcom	$⊢ (x \in A \lor \neg x \in C) \leftrightarrow (\neg x \in C \lor x \in A)$
12	11	anbi2i	$⊢ ((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 \lor x \in A))$
13	10 12	bitri	$⊢ (x \in A \lor (x \in B \land \neg x \in C)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
14	7 9 13	3bitri	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
15	5 6 14	3bitr4ri	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ (C ∖ A))$
16	15	eqriv	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A)$