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

Theorem fveq1d 5791
Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1d.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
fveq1d  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )

Proof of Theorem fveq1d
StepHypRef Expression
1 fveq1d.1 . 2  |-  ( ph  ->  F  =  G )
2 fveq1 5788 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524
This theorem is referenced by:  fveq12d  5795  funssfv  5804  csbfv12  5824  csbfv2g  5826  fvmptd  5878  fvmpt2d  5882  mpteqb  5887  fvmptt  5888  fnmptfvd  5905  fmptco  5975  fvunsn  6009  fvsng  6011  fsnunfv  6017  f1ocnvfv1  6082  f1ocnvfv2  6083  fcof1  6090  fcofo  6091  csbov123  6221  ofval  6429  offval2  6436  ofrfval2  6437  caofinvl  6447  curry1val  6765  curry2val  6769  fnwelem  6787  fvmpt2curryd  6890  rdg0g  6983  oav  7051  omv  7052  oev  7054  resixpfo  7401  pw2f1olem  7515  mapxpen  7577  xpmapenlem  7578  ordtypelem6  7838  ordtypelem7  7839  unwdomg  7900  cantnffval  7970  cantnfval  7977  cantnfres  7986  cantnfp1lem3  7989  cantnfvalOLD  8007  cantnfp1lem3OLD  8015  fseqenlem1  8295  fseqenlem2  8296  iunfictbso  8385  dfac12lem1  8413  dfac12lem2  8414  dfac12r  8416  ackbij2lem3  8511  ituni0  8688  itunisuc  8689  itunitc1  8690  ituniiun  8692  hsmexlem2  8697  hsmexlem4  8699  iundom2g  8805  konigthlem  8833  konigth  8834  fpwwe2lem6  8903  fpwwe2lem9  8906  rpnnen1lem3  11082  rpnnen1lem5  11084  fseq1p1m1  11635  seqp1  11922  seqf1olem2  11947  seqf1o  11948  seqid  11952  seqz  11955  seqof  11964  seqof2  11965  bcval5  12195  bcn2  12196  hashf1lem1  12310  seqcoll  12318  s1fv  12400  swrdfv  12422  swrdswrd  12456  splfv1  12499  revfv  12505  cshwidxmod  12542  shftcan1  12674  shftcan2  12675  climshft2  13162  isercoll2  13248  sumeq2w  13271  sumeq2ii  13272  summo  13296  fsum  13299  fsumss  13304  fsumcvg2  13306  isumsplit  13405  rpnnen2lem1  13599  rpnnen2  13610  ruclem4  13618  sadfval  13750  smufval  13775  odzval  13965  1arithlem2  14087  vdwpc  14143  vdwlem6  14149  ramval  14171  fvsetsid  14301  setsid  14317  setsnid  14318  prdsval  14495  prdsplusgfval  14514  prdsmulrfval  14516  pwsvscaval  14535  imasval  14551  xpsc0  14600  xpsc1  14601  mrisval  14670  comfffval  14739  sectffval  14791  invinv  14810  oppcsect  14814  brssc  14829  issubc  14850  isfunc  14876  funcoppc  14887  idfuval  14888  idfu2  14890  idfu1  14892  idfucl  14893  cofuval  14894  cofu1  14896  cofu2  14898  cofuval2  14899  cofucl  14900  cofurid  14903  resfval  14904  resfval2  14905  funcres  14908  funcpropd  14912  isfull  14922  isnat  14959  fucco  14974  homafval  14999  idafval  15027  setcmon  15057  catcisolem  15076  catciso  15077  xpcval  15089  1stf1  15104  2ndf1  15107  1stfcl  15109  2ndfcl  15110  prfval  15111  prf2fval  15113  prf1st  15116  prf2nd  15117  1st2ndprf  15118  evlf2  15130  evlf2val  15131  evlfcl  15134  curfval  15135  curfpropd  15145  uncfval  15146  uncf2  15149  curfuncf  15150  diag11  15155  diag12  15156  diag2  15157  curf2ndf  15159  hofval  15164  hofcl  15171  yon11  15176  yon12  15177  yon2  15178  yonedalem4a  15187  yonedalem4b  15188  yonedalem4c  15189  yonedalem22  15190  yonedalem3b  15191  yonedainv  15193  yoniso  15197  lubval  15256  glbval  15269  poslubdg  15421  prdspjmhm  15597  pwsco1mhm  15600  gsumvalx  15604  gsumpropd  15606  gsumress  15609  gsumval2a  15614  grpsubfval  15682  grplactval  15725  grpsubpropd  15728  grpsubpropd2  15729  mulgfval  15730  mulgpropd  15762  submmulg  15764  pwsinvg  15769  subgmulg  15797  eqgfval  15831  cntrval  15939  cntzval  15941  cntzrcl  15947  oppgsubg  15980  lactghmga  16011  symgga  16013  gsmsymgrfixlem1  16034  gsmsymgrfix  16035  gsmsymgreqlem1  16037  gsmsymgreqlem2  16038  gsmsymgreq  16039  pmtrval  16059  pmtrfv  16060  pmtrffv  16067  pmtrdifwrdellem3  16091  pmtrdifwrdel2lem1  16092  pmtrdifwrdel  16093  pmtrdifwrdel2  16094  ispgp  16195  vrgpval  16368  frgpup3lem  16378  frgpnabllem1  16455  frgpnabllem2  16456  gsumval3eu  16485  gsumval3OLD  16486  gsumval3lem2  16488  gsumval3  16489  gsumzres  16492  gsumzf1o  16495  gsumzresOLD  16496  gsumzf1oOLD  16498  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumconst  16532  dmdprd  16585  dprdval  16590  dprdvalOLD  16592  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprd2da  16646  dpjfval  16659  dpjidcl  16662  dpjlid  16665  dpjrid  16666  dpjidclOLD  16669  dvrfval  16882  staffval  17038  srngnvl  17047  issrngd  17052  lspval  17162  islbs  17263  lbspropd  17286  lssacsex  17331  lbsacsbs  17343  sralem  17364  srasca  17368  sravsca  17369  sraip  17370  rlmval  17378  ixpsnbasval  17396  lpival  17433  rrgsupp  17468  aspval  17505  psrmulval  17563  psrvscaval  17569  psrdi  17585  psrdir  17586  mvrval  17601  mvrval2  17602  mvrf1  17605  mplsubglem  17617  mplsubglemOLD  17619  mplvscaval  17634  subrgmvrf  17648  opsrle  17664  opsrbaslem  17666  subrgasclcl  17688  evlslem1  17708  evlsval  17712  evlssca  17715  evlsvar  17716  evlval  17717  evlsscasrng  17719  evlsvarsrng  17721  evlvar  17722  psr1val  17749  vr1val  17755  coe1fv  17769  subrgvr1  17822  coe1addfv  17826  coe1subfv  17827  coe1tmfv1  17835  coe1tmfv2  17836  coe1tmmul2fv  17839  coe1pwmulfv  17841  coe1sclmulfv  17844  ply1sclid  17849  ply1sclf1  17850  evls1val  17864  evls1sca  17867  evl1sca  17877  evl1scad  17878  evl1var  17879  evl1vard  17880  evls1var  17881  evls1scasrng  17882  evls1varsrng  17883  evl1addd  17884  evl1subd  17885  evl1muld  17886  evl1vsd  17887  evl1expd  17888  pf1ind  17898  evl1gsumdlem  17899  evl1gsumd  17900  evl1gsumadd  17901  zrhmulg  18050  chrval  18065  chrrhm  18071  znzrhval  18088  psgndiflemA  18140  ocvval  18201  elocv  18202  cssval  18216  pjfval  18240  pjfo  18249  isobs  18254  dsmmval  18268  dsmm0cl  18274  prdsinvgd2  18276  frlmvscaval  18303  frlmphl  18315  uvcval  18319  uvcvval  18320  uvcresum  18327  marepvval  18489  mdetfval  18508  mdetleib2  18510  mdet0fv0  18516  m1detdiag  18519  mdetdiaglem  18520  mdetralt  18530  mdetunilem7  18540  mdetuni0  18543  m2detleiblem1  18546  smadiadetr  18597  cramerimplem1  18605  ntrval  18756  clsval  18757  opncldf3  18806  neival  18822  neiptopreu  18853  lpfval  18858  lpval  18859  cnpval  18956  iscnp2  18959  isreg  19052  isnrm  19055  2ndcsep  19179  isnlly  19189  ptval  19259  dfac14  19307  cnmptk2  19375  pt1hmeo  19495  xkocnv  19503  fmval  19632  ufldom  19651  flimval  19652  flffval  19678  flfval  19679  cnpflf  19690  txflf  19695  fclsval  19697  fcfval  19722  cnextval  19749  cnextfvval  19753  cnextcn  19755  cnextfres  19756  symgtgp  19788  tgpconcomp  19799  prdstmdd  19810  utopsnneiplem  19938  neipcfilu  19987  txmetcnp  20238  subgnm2  20336  tngngp  20356  isnlm  20372  sranlm  20381  lssnlm  20397  nmofval  20409  nmoval  20410  isphtpy  20669  pcovalg  20700  pco1  20703  clmneg  20769  clmabs  20770  nmoleub2lem3  20786  nmoleub3  20790  cphcjcl  20818  cphnm  20828  cphipcj  20834  cphassr  20846  tchnmval  20860  tchcphlem3  20864  ipcau2  20865  tchcphlem1  20866  tchcphlem2  20867  tchcph  20868  ipcau  20869  rrxnm  21011  ovolctb  21089  voliunlem3  21149  uniioombllem2  21179  vitalilem4  21207  mbflimsup  21260  itg1climres  21308  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1fseqlem6  21314  mbfi1flimlem  21316  mbfmullem2  21318  mbfmullem  21319  itg2monolem1  21344  itg2mono  21347  itg2i1fseqle  21348  itg2i1fseq  21349  itg2addlem  21352  itg2cnlem1  21355  limcfval  21463  limcmpt2  21475  limcres  21477  cnplimc  21478  dvfval  21488  dvreslem  21500  dvres2lem  21501  dvn0  21514  dvnp1  21515  cpnfval  21522  elcpn  21524  dvaddbr  21528  dvmulbr  21529  dvcmul  21534  dvfre  21541  rolle  21578  cmvth  21579  mvth  21580  dvlip  21581  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  dveq0  21588  dv11cn  21589  dvivthlem1  21596  dvivth  21598  dvne0  21599  lhop1lem  21601  lhop2  21603  lhop  21604  dvcnvrelem2  21606  dvcvx  21608  dvfsumabs  21611  ftc1lem6  21629  ftc2  21632  ftc2ditglem  21633  itgparts  21635  itgsubstlem  21636  mdegaddle  21661  mdegmullem  21665  coe1mul3  21687  uc1pval  21727  mon1pval  21729  uc1pmon1p  21739  q1pval  21741  ply1remlem  21750  ply1rem  21751  fta1glem2  21754  fta1g  21755  fta1blem  21756  ig1pval  21760  plyeq0lem  21794  coeeulem  21808  coeid2  21823  dgrle  21827  dgreq  21828  0dgrb  21830  coemul  21835  coe11  21836  coe1term  21842  dgrlt  21849  dgradd2  21851  dgrcolem2  21857  plymul0or  21863  plydivlem4  21878  plydiveu  21880  plyremlem  21886  plyrem  21887  fta1  21890  vieta1lem2  21893  plyexmo  21895  aareccl  21908  aannenlem1  21910  aannenlem2  21911  taylfval  21940  tayl0  21943  dvtaylp  21951  dvntaylp0  21953  taylthlem1  21954  taylthlem2  21955  ulmval  21961  ulmres  21969  ulmshftlem  21970  ulmshft  21971  ulmuni  21973  ulmcaulem  21975  ulmcau  21976  ulmss  21978  ulmdvlem1  21981  ulmdvlem3  21983  mtest  21985  mtestbdd  21986  mbfulm  21987  itgulm  21989  itgulm2  21990  pserval2  21992  pserulm  22003  psercn  22007  pserdvlem2  22009  pserdv  22010  pige3  22095  logtayl  22221  rlimcnp  22475  sqff1o  22636  muinv  22649  dchrinv  22716  sumdchr2  22725  dchr2sum  22728  lgsval4  22771  lgsmod  22776  lgsqrlem1  22796  dchrmusumlema  22858  dchrvmasumlem1  22860  dchrisum0re  22878  dchrisum0lema  22879  logsqvma2  22908  padicval  22982  iscgrg  23084  midexlem  23212  colperplem2  23241  colperplem3  23242  mideulem  23244  mideu  23245  brcgr  23281  ecgrtg  23364  vdgrfval  23700  vdgrval  23701  iseupa  23721  eupath2lem3  23735  eupath2  23736  grpoinvval  23847  grpodivfval  23864  gxfval  23879  gxval  23880  imsdval  24212  sspnval  24270  nmoofval  24297  nmooval  24298  bloval  24316  0oval  24323  nmlno0  24330  hmoval  24345  ajval  24397  ubth  24409  htthlem  24454  pjhval  24935  pjoc1  24972  pjoc2  24977  pjige0  25229  pjcjt2  25230  pjch  25232  pjsumi  25248  pjdsi  25250  pjds3i  25251  pjopyth  25258  pjnorm  25262  pjpyth  25263  pjnel  25264  hosval  25279  homval  25280  hodval  25281  hfsval  25282  hfmval  25283  braval  25483  kbval  25493  eigvalval  25499  leopg  25661  leoppos  25665  leoprf2  25666  leoprf  25667  elpjrn  25729  pj3cor1i  25748  strlem2  25790  hstrlem2  25798  fmptcof2  26113  offval2f  26117  resf1o  26164  fpwrelmap  26167  fmcncfil  26495  nmmulg  26531  zrhnm  26532  qqhval  26537  qqhcn  26554  ofcfval  26674  ofcfval3  26678  brfae  26798  omsval  26842  sitgval  26852  eulerpartlemsv1  26873  eulerpartlemsf  26876  eulerpartlemgvv  26893  eulerpartlemn  26898  sseqval  26905  sseqfv1  26906  sseqfv2  26911  fibp1  26918  dstrvval  26987  ballotleme  27013  ballotlemi  27017  plymulx0  27082  plymulx  27083  signstfv  27098  signstfvneq0  27107  signstfvc  27109  signstres  27110  signstfveq0  27112  lgamgulmlem2  27150  lgamgulmlem5  27153  lgamgulm2  27156  lgamcvglem  27160  subfacp1lem5  27206  kur14  27238  ptpcon  27256  cvmliftmolem1  27304  cvmliftlem5  27312  cvmliftlem7  27314  cvmliftlem15  27321  cvmlift2lem3  27328  cvmlift2lem4  27329  cvmlift2lem7  27332  cvmlift2lem9  27334  cvmlift2  27339  cvmliftphtlem  27340  cvmlift3lem2  27343  cvmlift3lem5  27346  cvmlift3lem6  27347  cvmlift3lem7  27348  cvmlift3lem9  27350  cvmlift3  27351  relexp0  27465  relexpsucr  27466  shftvalg  27529  prodeq2w  27559  prodeq2ii  27560  prodmo  27583  fprod  27588  fprodss  27595  bpolylem  28325  ftc2nc  28614  neibastop3  28721  tailval  28732  filnetlem4  28740  cocanfo  28749  f1ocan2fv  28759  upixp  28761  sdclem2  28776  rrncmslem  28869  ismrer1  28875  isnacs  29178  mzpsubst  29223  eldioph2  29238  pw2f1ocnv  29524  fnwe2lem2  29542  islnr3  29609  hbtlem1  29617  hbtlem2  29618  hbtlem7  29619  hbtlem4  29620  hbtlem5  29622  hbt  29624  dgrsub2  29629  dgrnznn  29630  mpaaeu  29645  mpaalem  29647  rgspnval  29663  flcidc  29669  cntzsdrg  29697  itgpowd  29728  addrfv  29863  subrfv  29864  mulvfv  29865  refsum2cnlem1  29897  fmuldfeqlem1  29901  fmuldfeq  29902  fmul01lt1lem1  29903  fmul01lt1lem2  29904  stoweidlem17  29950  stoweidlem20  29953  stoweidlem27  29960  stoweidlem31  29964  stoweidlem34  29967  stoweidlem44  29977  stoweidlem48  29981  stoweidlem59  29992  stirlinglem3  30009  stirlinglem15  30021  elovmpt3rab1  30301  ccatw2s1p1  30407  ccatw2s1p2  30408  ccat2s1fvw  30409  wwlkn  30454  wlkiswwlkfun  30487  wlkiswwlkinj  30488  wlkiswwlksur  30489  wlkiswwlkbij2  30491  clwwlkn  30568  isrgra  30681  rusgranumwlklem4  30708  vdfrgra0  30752  vdgfrgra0  30753  ply1coe1eq  30978  coe1fzgsumdlem  30979  coe1fzgsumd  30980  coe1sclmulval  30981  gsummoncoe1  30985  ply1mulgsum  30990  cply1coe0bi  30992  gsumply1eq  30994  evl1at0  30995  evl1at1  30996  mat1dimscm  31025  lincvalpr  31059  cpmatel  31174  1elcpmat  31178  cpmatinvcl  31180  cpmatmcllem  31181  cpmatmcl  31182  mat2pmatfval  31186  m2cpm  31204  m2pminvval  31210  m2pminv  31211  m2pminv2lem  31212  m2pminv2  31213  pmatcollpw1lem3  31225  pmatcollpw1id  31226  pmatcollpw1dstlem1  31227  pmatcollpw1dst  31228  pmatcollpwfsupp  31229  pmatcollpw1  31232  pmatcollpwlem  31233  pmatcollpw1aa0  31235  monmatcollpw  31236  pmatcollpw4  31240  pmatcollpw4fi  31241  pmatcollpwscmatlem1  31245  pmatcollpwscmatlem3  31247  mply1topmatval  31251  pmattomply1ghmlem2  31254  pmattomply1f1lem  31255  pmattomply1rn  31257  pmattomply1coe1  31259  idpmattoidmply1  31260  mp2pm2mplem1  31261  mp2pm2mplem3  31263  mp2pm2mplem4  31264  mp2pm2mplem5  31265  mp2pm2mp  31266  pmattomply1f1  31267  pmattomply1fo  31268  pmattomply1ghm  31270  pmattomply1mhmlem0  31272  pmattomply1mhmlem1  31273  pmattomply1mhmlem2  31274  monmat2matmon  31278  cpmatfval  31283  cpmat0d  31288  cpscmatgsumbin  31298  cpmidgsum  31322  cpmadugsumfi  31331  cpmadumatpolylem2  31336  chcoeffeq  31341  cayleyhamilton0  31344  cayleyhamilton  31345  cayleyhamiltonALT  31346  bnj1379  32124  bj-finsumval0  32889  lshpset  32929  lsatset  32941  lkrval  33039  eqlkr  33050  ldualvaddval  33082  ldualvsval  33089  ldualvsubval  33108  cmtfvalN  33161  isoml  33189  pmapval  33707  pclvalN  33840  polfvalN  33854  polvalN  33855  psubclsetN  33886  watfvalN  33942  watvalN  33943  ldilset  34059  ltrnfset  34067  ltrnset  34068  dilfsetN  34102  dilsetN  34103  trnfsetN  34105  trnsetN  34106  trlfset  34110  trlset  34111  trlval  34112  ltrnideq  34125  cdlemd8  34155  cdlemg1idlemN  34522  cdlemg1fvawlemN  34523  cdlemg2idN  34546  trlcoabs2N  34672  tgrpfset  34694  tgrpset  34695  tendofset  34708  tendoset  34709  erngfset  34749  erngset  34750  erngfset-rN  34757  erngset-rN  34758  cdlemi2  34769  cdlemj1  34771  cdlemk2  34782  cdlemk4  34784  cdlemk8  34788  cdlemkuu  34845  cdlemk31  34846  cdlemkuv2-3N  34849  cdlemk18-3N  34850  cdlemk22-3  34851  cdlemkfid2N  34873  cdlemkyu  34877  cdlemk19ylem  34880  cdlemk46  34898  cdlemk49  34901  cdlemk43N  34913  cdlemk19u1  34919  cdlemk19u  34920  dvafset  34954  dvaset  34955  dvaplusgv  34960  diaffval  34981  diafval  34982  diaval  34983  dvhfset  35031  dvhset  35032  dvhlveclem  35059  docaffvalN  35072  docafvalN  35073  docavalN  35074  djaffvalN  35084  djafvalN  35085  dibffval  35091  dibfval  35092  dibval  35093  dicffval  35125  dicfval  35126  dicval  35127  dicelvalN  35129  dicvaddcl  35141  dicvscacl  35142  cdlemn8  35155  cdlemn9  35156  dihordlem7b  35166  dihffval  35181  dihfval  35182  dihval  35183  dihopelvalcpre  35199  dihmeetlem1N  35241  dihglblem5apreN  35242  dihmeetlem4preN  35257  dihmeetlem13N  35270  dih1dimatlem0  35279  dochffval  35300  dochfval  35301  dochval  35302  djhffval  35347  djhfval  35348  lcfl7lem  35450  lclkrlem2k  35468  lclkrlem2u  35478  lcdfval  35539  lcdval  35540  lcdvaddval  35549  lcdvsval  35555  lcd0vvalN  35564  lcdvsubval  35569  lcdlsp  35572  mapdffval  35577  mapdfval  35578  mapdval  35579  hvmapffval  35709  hvmapfval  35710  hvmapval  35711  hvmapvalvalN  35712  hvmapidN  35713  hvmaplkr  35719  hdmap1ffval  35747  hdmap1fval  35748  hdmap1vallem  35749  hdmapffval  35780  hdmapfval  35781  hdmapval  35782  hdmapevec2  35790  hgmapffval  35839  hgmapfval  35840  hgmapval  35841  hdmaplna2  35864  hdmapglnm2  35865  hdmapinvlem3  35874  hlhilset  35888  hlhilipval  35903
  Copyright terms: Public domain W3C validator