Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ofval Structured version   Unicode version

Theorem ofval 6306
 Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)
Hypotheses
Ref Expression
offval.1
offval.2
offval.3
offval.4
offval.5
ofval.6
ofval.7
Assertion
Ref Expression
ofval

Proof of Theorem ofval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 offval.1 . . . . 5
2 offval.2 . . . . 5
3 offval.3 . . . . 5
4 offval.4 . . . . 5
5 offval.5 . . . . 5
6 eqidd 2436 . . . . 5
7 eqidd 2436 . . . . 5
81, 2, 3, 4, 5, 6, 7offval 6304 . . . 4
98fveq1d 5722 . . 3
109adantr 452 . 2
11 fveq2 5720 . . . . 5
12 fveq2 5720 . . . . 5
1311, 12oveq12d 6091 . . . 4
14 eqid 2435 . . . 4
15 ovex 6098 . . . 4
1613, 14, 15fvmpt 5798 . . 3
1716adantl 453 . 2
18 inss1 3553 . . . . . 6
195, 18eqsstr3i 3371 . . . . 5
2019sseli 3336 . . . 4
21 ofval.6 . . . 4
2220, 21sylan2 461 . . 3
23 inss2 3554 . . . . . 6
245, 23eqsstr3i 3371 . . . . 5
2524sseli 3336 . . . 4
26 ofval.7 . . . 4
2725, 26sylan2 461 . . 3
2822, 27oveq12d 6091 . 2
2910, 17, 283eqtrd 2471 1