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