Description: Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | uniuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni | |
|
2 | 1 | anbi2i | |
3 | 2 | exbii | |
4 | 19.42v | |
|
5 | 4 | bicomi | |
6 | 5 | exbii | |
7 | excom | |
|
8 | anass | |
|
9 | ancom | |
|
10 | 8 9 | bitr3i | |
11 | 10 | 2exbii | |
12 | exdistr | |
|
13 | 7 11 12 | 3bitri | |
14 | eluni | |
|
15 | 14 | bicomi | |
16 | 15 | anbi2i | |
17 | 16 | exbii | |
18 | 6 13 17 | 3bitri | |
19 | vuniex | |
|
20 | eleq2 | |
|
21 | 19 20 | ceqsexv | |
22 | exancom | |
|
23 | 21 22 | bitr3i | |
24 | 23 | anbi2i | |
25 | 19.42v | |
|
26 | ancom | |
|
27 | anass | |
|
28 | 26 27 | bitri | |
29 | 28 | exbii | |
30 | 24 25 29 | 3bitr2i | |
31 | 30 | exbii | |
32 | excom | |
|
33 | exdistr | |
|
34 | vex | |
|
35 | eqeq1 | |
|
36 | 35 | anbi1d | |
37 | 36 | exbidv | |
38 | 34 37 | elab | |
39 | 38 | bicomi | |
40 | 39 | anbi2i | |
41 | 40 | exbii | |
42 | 33 41 | bitri | |
43 | 31 32 42 | 3bitri | |
44 | 3 18 43 | 3bitri | |
45 | 44 | abbii | |
46 | df-uni | |
|
47 | df-uni | |
|
48 | 45 46 47 | 3eqtr4i | |