Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ofcfval.1 | |
|
ofcfval.2 | |
||
ofcfval.3 | |
||
ofcfval.6 | |
||
Assertion | ofcfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ofcfval.1 | |
|
2 | ofcfval.2 | |
|
3 | ofcfval.3 | |
|
4 | ofcfval.6 | |
|
5 | df-ofc | |
|
6 | 5 | a1i | |
7 | simprl | |
|
8 | 7 | dmeqd | |
9 | 7 | fveq1d | |
10 | simprr | |
|
11 | 9 10 | oveq12d | |
12 | 8 11 | mpteq12dv | |
13 | fnex | |
|
14 | 1 2 13 | syl2anc | |
15 | 3 | elexd | |
16 | 1 | fndmd | |
17 | 16 2 | eqeltrd | |
18 | 17 | mptexd | |
19 | 6 12 14 15 18 | ovmpod | |
20 | 16 | eleq2d | |
21 | 20 | pm5.32i | |
22 | 21 4 | sylbi | |
23 | 22 | oveq1d | |
24 | 16 23 | mpteq12dva | |
25 | 19 24 | eqtrd | |