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

Theorem ofval 6549
 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 2458 . . . . 5
7 eqidd 2458 . . . . 5
81, 2, 3, 4, 5, 6, 7offval 6547 . . . 4
98fveq1d 5873 . . 3
11 fveq2 5871 . . . . 5
12 fveq2 5871 . . . . 5
1311, 12oveq12d 6314 . . . 4
14 eqid 2457 . . . 4
15 ovex 6324 . . . 4
1613, 14, 15fvmpt 5956 . . 3
18 inss1 3717 . . . . . 6
195, 18eqsstr3i 3534 . . . . 5
2019sseli 3499 . . . 4
21 ofval.6 . . . 4
2220, 21sylan2 474 . . 3
23 inss2 3718 . . . . . 6
245, 23eqsstr3i 3534 . . . . 5
2524sseli 3499 . . . 4
26 ofval.7 . . . 4
2725, 26sylan2 474 . . 3
2822, 27oveq12d 6314 . 2
2910, 17, 283eqtrd 2502 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474  e.cmpt 4510  Fnwfn 5588  cfv 5593  (class class class)co 6296  oF`cof 6538 This theorem is referenced by:  fnfvof  6553  offveq  6561  ofc1  6563  ofc2  6564  suppofss1d  6956  suppofss2d  6957  ofsubeq0  10558  ofnegsub  10559  ofsubge0  10560  seqof  12164  o1of2  13435  gsumzaddlem  16934  gsumzaddlemOLD  16936  psrbagcon  18022  psrbagconf1o  18026  psrdi  18061  psrdir  18062  mplsubglem  18093  mplsubglemOLD  18095  matplusgcell  18935  matsubgcell  18936  rrxcph  21824  mbfaddlem  22067  i1faddlem  22100  i1fmullem  22101  itg1lea  22119  mbfi1flimlem  22129  itg2split  22156  itg2monolem1  22157  itg2addlem  22165  dvaddbr  22341  dvmulbr  22342  plyaddlem1  22610  coeeulem  22621  coeaddlem  22646  dgradd2  22665  dgrcolem2  22671  ofmulrt  22678  plydivlem3  22691  plydivlem4  22692  plydiveu  22694  plyrem  22701  vieta1lem2  22707  elqaalem3  22717  qaa  22719  basellem7  23360  basellem9  23362  itg2addnclem3  30068  itg2addnc  30069  ftc1anclem5  30094  dgrsub2  31084  mpaaeu  31099  caofcan  31228  ofmul12  31230  ofdivrec  31231  ofdivcan4  31232  ofdivdiv2  31233  binomcxplemrat  31255  binomcxplemnotnn0  31261  mndpsuppss  32964  lfladdcl  34796  ldualvaddval  34856 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pr 4691 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6540
 Copyright terms: Public domain W3C validator