Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fourierdlem2.1 | |
|
Assertion | fourierdlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fourierdlem2.1 | |
|
2 | oveq2 | |
|
3 | 2 | oveq2d | |
4 | fveqeq2 | |
|
5 | 4 | anbi2d | |
6 | oveq2 | |
|
7 | 6 | raleqdv | |
8 | 5 7 | anbi12d | |
9 | 3 8 | rabeqbidv | |
10 | ovex | |
|
11 | 10 | rabex | |
12 | 9 1 11 | fvmpt | |
13 | 12 | eleq2d | |
14 | fveq1 | |
|
15 | 14 | eqeq1d | |
16 | fveq1 | |
|
17 | 16 | eqeq1d | |
18 | 15 17 | anbi12d | |
19 | fveq1 | |
|
20 | fveq1 | |
|
21 | 19 20 | breq12d | |
22 | 21 | ralbidv | |
23 | 18 22 | anbi12d | |
24 | 23 | elrab | |
25 | 13 24 | bitrdi | |