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 AC=BCAC=BCA=B

Proof

Step Hyp Ref Expression
1 eleq2 AC=BCxACxBC
2 elin xACxAxC
3 elin xBCxBxC
4 1 2 3 3bitr3g AC=BCxAxCxBxC
5 iba xCxAxAxC
6 iba xCxBxBxC
7 5 6 bibi12d xCxAxBxAxCxBxC
8 4 7 imbitrrid xCAC=BCxAxB
9 8 adantld xCAC=BCAC=BCxAxB
10 uncom AC=CA
11 uncom BC=CB
12 10 11 eqeq12i AC=BCCA=CB
13 eleq2 CA=CBxCAxCB
14 12 13 sylbi AC=BCxCAxCB
15 elun xCAxCxA
16 elun xCBxCxB
17 14 15 16 3bitr3g AC=BCxCxAxCxB
18 biorf ¬xCxAxCxA
19 biorf ¬xCxBxCxB
20 18 19 bibi12d ¬xCxAxBxCxAxCxB
21 17 20 imbitrrid ¬xCAC=BCxAxB
22 21 adantrd ¬xCAC=BCAC=BCxAxB
23 9 22 pm2.61i AC=BCAC=BCxAxB
24 23 eqrdv AC=BCAC=BCA=B
25 uneq1 A=BAC=BC
26 ineq1 A=BAC=BC
27 25 26 jca A=BAC=BCAC=BC
28 24 27 impbii AC=BCAC=BCA=B