Metamath Proof Explorer

Theorem unineq

Description: Infer equality from equalities of union and intersection. Exercise 20 of Enderton p. 32 and its converse. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion unineq ⊢ A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C ↔ A = B

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ A ∩ C = B ∩ C → x ∈ A ∩ C ↔ x ∈ B ∩ C
2 elin ⊢ x ∈ A ∩ C ↔ x ∈ A ∧ x ∈ C
3 elin ⊢ x ∈ B ∩ C ↔ x ∈ B ∧ x ∈ C
4 1 2 3 3bitr3g ⊢ A ∩ C = B ∩ C → x ∈ A ∧ x ∈ C ↔ x ∈ B ∧ x ∈ C
5 iba ⊢ x ∈ C → x ∈ A ↔ x ∈ A ∧ x ∈ C
6 iba ⊢ x ∈ C → x ∈ B ↔ x ∈ B ∧ x ∈ C
7 5 6 bibi12d ⊢ x ∈ C → x ∈ A ↔ x ∈ B ↔ x ∈ A ∧ x ∈ C ↔ x ∈ B ∧ x ∈ C
8 4 7 imbitrrid ⊢ x ∈ C → A ∩ C = B ∩ C → x ∈ A ↔ x ∈ B
9 8 adantld ⊢ x ∈ C → A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C → x ∈ A ↔ x ∈ B
10 uncom ⊢ A ∪ C = C ∪ A
11 uncom ⊢ B ∪ C = C ∪ B
12 10 11 eqeq12i ⊢ A ∪ C = B ∪ C ↔ C ∪ A = C ∪ B
13 eleq2 ⊢ C ∪ A = C ∪ B → x ∈ C ∪ A ↔ x ∈ C ∪ B
14 12 13 sylbi ⊢ A ∪ C = B ∪ C → x ∈ C ∪ A ↔ x ∈ C ∪ B
15 elun ⊢ x ∈ C ∪ A ↔ x ∈ C ∨ x ∈ A
16 elun ⊢ x ∈ C ∪ B ↔ x ∈ C ∨ x ∈ B
17 14 15 16 3bitr3g ⊢ A ∪ C = B ∪ C → x ∈ C ∨ x ∈ A ↔ x ∈ C ∨ x ∈ B
18 biorf ⊢ ¬ x ∈ C → x ∈ A ↔ x ∈ C ∨ x ∈ A
19 biorf ⊢ ¬ x ∈ C → x ∈ B ↔ x ∈ C ∨ x ∈ B
20 18 19 bibi12d ⊢ ¬ x ∈ C → x ∈ A ↔ x ∈ B ↔ x ∈ C ∨ x ∈ A ↔ x ∈ C ∨ x ∈ B
21 17 20 imbitrrid ⊢ ¬ x ∈ C → A ∪ C = B ∪ C → x ∈ A ↔ x ∈ B
22 21 adantrd ⊢ ¬ x ∈ C → A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C → x ∈ A ↔ x ∈ B
23 9 22 pm2.61i ⊢ A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C → x ∈ A ↔ x ∈ B
24 23 eqrdv ⊢ A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C → A = B
25 uneq1 ⊢ A = B → A ∪ C = B ∪ C
26 ineq1 ⊢ A = B → A ∩ C = B ∩ C
27 25 26 jca ⊢ A = B → A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C
28 24 27 impbii ⊢ A ∪ C = B ∪ C ∧ A ∩ C = B ∩ C ↔ A = B