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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | |
|
2 | elin | |
|
3 | elin | |
|
4 | 1 2 3 | 3bitr3g | |
5 | iba | |
|
6 | iba | |
|
7 | 5 6 | bibi12d | |
8 | 4 7 | imbitrrid | |
9 | 8 | adantld | |
10 | uncom | |
|
11 | uncom | |
|
12 | 10 11 | eqeq12i | |
13 | eleq2 | |
|
14 | 12 13 | sylbi | |
15 | elun | |
|
16 | elun | |
|
17 | 14 15 16 | 3bitr3g | |
18 | biorf | |
|
19 | biorf | |
|
20 | 18 19 | bibi12d | |
21 | 17 20 | imbitrrid | |
22 | 21 | adantrd | |
23 | 9 22 | pm2.61i | |
24 | 23 | eqrdv | |
25 | uneq1 | |
|
26 | ineq1 | |
|
27 | 25 26 | jca | |
28 | 24 27 | impbii | |