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 ∪ B ∖ C = A ∪ B ∖ C ∖ A

Proof

Step Hyp Ref Expression
1 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
2 pm4.53 ⊢ ¬ x ∈ C ∧ ¬ x ∈ A ↔ ¬ x ∈ C ∨ x ∈ A
3 eldif ⊢ x ∈ C ∖ A ↔ x ∈ C ∧ ¬ x ∈ A
4 2 3 xchnxbir ⊢ ¬ x ∈ C ∖ A ↔ ¬ x ∈ C ∨ x ∈ A
5 1 4 anbi12i ⊢ x ∈ A ∪ B ∧ ¬ x ∈ C ∖ A ↔ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ∨ x ∈ A
6 eldif ⊢ x ∈ A ∪ B ∖ C ∖ A ↔ x ∈ A ∪ B ∧ ¬ x ∈ C ∖ A
7 elun ⊢ x ∈ A ∪ B ∖ C ↔ x ∈ A ∨ x ∈ B ∖ C
8 eldif ⊢ x ∈ B ∖ C ↔ x ∈ B ∧ ¬ x ∈ C
9 8 orbi2i ⊢ x ∈ A ∨ x ∈ B ∖ C ↔ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C
10 ordi ⊢ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ↔ x ∈ A ∨ x ∈ B ∧ x ∈ A ∨ ¬ x ∈ C
11 orcom ⊢ x ∈ A ∨ ¬ x ∈ C ↔ ¬ x ∈ C ∨ x ∈ A
12 11 anbi2i ⊢ x ∈ A ∨ x ∈ B ∧ x ∈ A ∨ ¬ x ∈ C ↔ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ∨ x ∈ A
13 10 12 bitri ⊢ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ↔ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ∨ x ∈ A
14 7 9 13 3bitri ⊢ x ∈ A ∪ B ∖ C ↔ x ∈ A ∨ x ∈ B ∧ ¬ x ∈ C ∨ x ∈ A
15 5 6 14 3bitr4ri ⊢ x ∈ A ∪ B ∖ C ↔ x ∈ A ∪ B ∖ C ∖ A
16 15 eqriv ⊢ A ∪ B ∖ C = A ∪ B ∖ C ∖ A