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

Theorem ofval 6554
 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 2430 . . . . 5
7 eqidd 2430 . . . . 5
81, 2, 3, 4, 5, 6, 7offval 6552 . . . 4
98fveq1d 5883 . . 3
11 fveq2 5881 . . . . 5
12 fveq2 5881 . . . . 5
1311, 12oveq12d 6323 . . . 4
14 eqid 2429 . . . 4
15 ovex 6333 . . . 4
1613, 14, 15fvmpt 5964 . . 3
18 inss1 3688 . . . . . 6
195, 18eqsstr3i 3501 . . . . 5
2019sseli 3466 . . . 4
21 ofval.6 . . . 4
2220, 21sylan2 476 . . 3
23 inss2 3689 . . . . . 6
245, 23eqsstr3i 3501 . . . . 5
2524sseli 3466 . . . 4
26 ofval.7 . . . 4
2725, 26sylan2 476 . . 3
2822, 27oveq12d 6323 . 2
2910, 17, 283eqtrd 2474 1