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

Theorem fveq1d 5858
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 5855 . 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 1383   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586
This theorem is referenced by:  fveq12d  5862  funssfv  5871  csbfv12  5891  csbfv2g  5893  fvmptd  5946  fvmpt2d  5950  mpteqb  5955  fvmptt  5956  fnmptfvd  5975  fmptco  6049  fvunsn  6088  fvsng  6090  fsnunfv  6096  f1ocnvfv1  6167  f1ocnvfv2  6168  fcof1  6175  fcofo  6176  csbov123  6315  elovmpt3rab1  6521  ofval  6534  offval2  6541  ofrfval2  6542  caofinvl  6552  curry1val  6878  curry2val  6882  fnwelem  6900  fvmpt2curryd  7002  rdg0g  7095  oav  7163  omv  7164  oev  7166  resixpfo  7509  pw2f1olem  7623  mapxpen  7685  xpmapenlem  7686  ordtypelem6  7951  ordtypelem7  7952  unwdomg  8013  cantnffval  8083  cantnfval  8090  cantnfres  8099  cantnfp1lem3  8102  cantnfvalOLD  8120  cantnfp1lem3OLD  8128  fseqenlem1  8408  fseqenlem2  8409  iunfictbso  8498  dfac12lem1  8526  dfac12lem2  8527  dfac12r  8529  ackbij2lem3  8624  ituni0  8801  itunisuc  8802  itunitc1  8803  ituniiun  8805  hsmexlem2  8810  hsmexlem4  8812  iundom2g  8918  konigthlem  8946  konigth  8947  fpwwe2lem6  9016  fpwwe2lem9  9019  rpnnen1lem3  11221  rpnnen1lem5  11223  fseq1p1m1  11763  seqp1  12104  seqf1olem2  12129  seqf1o  12130  seqid  12134  seqz  12137  seqof  12146  seqof2  12147  bcval5  12378  bcn2  12379  hashf1lem1  12486  seqcoll  12494  s1fv  12601  ccatw2s1p1  12622  ccatw2s1p2  12623  swrdfv  12633  swrdswrd  12667  splfv1  12713  revfv  12719  cshwidxmod  12756  ccat2s1fvwALT  12875  shftcan1  12898  shftcan2  12899  climshft2  13387  isercoll2  13473  sumeq2w  13496  sumeq2ii  13497  summo  13521  fsum  13524  fsumss  13529  fsumcvg2  13531  isumsplit  13634  prodeq2w  13701  prodeq2ii  13702  prodmo  13725  fprod  13730  fprodss  13737  rpnnen2lem1  13930  rpnnen2  13941  ruclem4  13949  sadfval  14084  smufval  14109  odzval  14300  1arithlem2  14424  vdwpc  14480  vdwlem6  14486  ramval  14508  fvsetsid  14639  setsid  14655  setsnid  14656  prdsval  14834  prdsplusgfval  14853  prdsmulrfval  14855  pwsvscaval  14874  imasval  14890  xpsc0  14939  xpsc1  14940  mrisval  15009  comfffval  15075  sectffval  15127  invinv  15146  oppcsect  15150  brssc  15165  issubc  15186  isfunc  15212  funcoppc  15223  idfuval  15224  idfu2  15226  idfu1  15228  idfucl  15229  cofuval  15230  cofu1  15232  cofu2  15234  cofuval2  15235  cofucl  15236  cofurid  15239  resfval  15240  resfval2  15241  funcres  15244  funcpropd  15248  isfull  15258  isnat  15295  fucco  15310  homafval  15335  idafval  15363  setcmon  15393  catcisolem  15412  catciso  15413  xpcval  15425  1stf1  15440  2ndf1  15443  1stfcl  15445  2ndfcl  15446  prfval  15447  prf2fval  15449  prf1st  15452  prf2nd  15453  1st2ndprf  15454  evlf2  15466  evlf2val  15467  evlfcl  15470  curfval  15471  curfpropd  15481  uncfval  15482  uncf2  15485  curfuncf  15486  diag11  15491  diag12  15492  diag2  15493  curf2ndf  15495  hofval  15500  hofcl  15507  yon11  15512  yon12  15513  yon2  15514  yonedalem4a  15523  yonedalem4b  15524  yonedalem4c  15525  yonedalem22  15526  yonedalem3b  15527  yonedainv  15529  yoniso  15533  lubval  15593  glbval  15606  poslubdg  15758  gsumvalx  15876  gsumpropd  15878  gsumress  15882  gsumval2a  15885  prdspjmhm  15977  pwsco1mhm  15980  grpsubfval  16071  grplactval  16116  grpsubpropd  16119  grpsubpropd2  16120  mulgfval  16122  mulgpropd  16154  submmulg  16156  pwsinvg  16161  subgmulg  16194  eqgfval  16228  cntrval  16336  cntzval  16338  cntzrcl  16344  oppgsubg  16377  lactghmga  16408  symgga  16410  gsmsymgrfixlem1  16431  gsmsymgrfix  16432  gsmsymgreqlem1  16434  gsmsymgreqlem2  16435  gsmsymgreq  16436  pmtrval  16455  pmtrfv  16456  pmtrffv  16463  pmtrdifwrdellem3  16487  pmtrdifwrdel2lem1  16488  pmtrdifwrdel  16489  pmtrdifwrdel2  16490  ispgp  16591  vrgpval  16764  frgpup3lem  16774  frgpnabllem1  16856  frgpnabllem2  16857  gsumval3eu  16886  gsumval3OLD  16887  gsumval3lem2  16889  gsumval3  16890  gsumzres  16893  gsumzf1o  16896  gsumzresOLD  16897  gsumzf1oOLD  16899  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  dmdprd  17008  dprdval  17013  dprdvalOLD  17015  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  dprd2da  17070  dpjfval  17083  dpjidcl  17086  dpjlid  17089  dpjrid  17090  dpjidclOLD  17093  dvrfval  17312  staffval  17475  srngnvl  17484  issrngd  17489  lspval  17600  islbs  17701  lbspropd  17724  lssacsex  17769  lbsacsbs  17781  sralem  17802  srasca  17806  sravsca  17807  sraip  17808  rlmval  17816  ixpsnbasval  17834  lpival  17872  rrgsupp  17918  aspval  17956  psrmulval  18018  psrvscaval  18024  psrdi  18040  psrdir  18041  mvrval  18056  mvrval2  18057  mvrf1  18060  mplsubglem  18072  mplsubglemOLD  18074  mplvscaval  18089  subrgmvrf  18103  opsrle  18119  opsrbaslem  18121  subrgasclcl  18143  evlslem1  18163  evlsval  18167  evlssca  18170  evlsvar  18171  evlval  18172  evlsscasrng  18174  evlsvarsrng  18176  evlvar  18177  psr1val  18204  vr1val  18210  coe1fv  18224  subrgvr1  18281  coe1addfv  18285  coe1subfv  18286  coe1tmfv1  18294  coe1tmfv2  18295  coe1tmmul2fv  18298  coe1pwmulfv  18300  coe1sclmulfv  18303  ply1sclid  18308  ply1sclf1  18309  ply1coe1eq  18319  cply1coe0bi  18321  coe1fzgsumdlem  18322  coe1fzgsumd  18323  gsummoncoe1  18325  gsumply1eq  18326  evls1val  18336  evls1sca  18339  evl1sca  18349  evl1scad  18350  evl1var  18351  evl1vard  18352  evls1var  18353  evls1scasrng  18354  evls1varsrng  18355  evl1addd  18356  evl1subd  18357  evl1muld  18358  evl1vsd  18359  evl1expd  18360  pf1ind  18370  evl1gsumdlem  18371  evl1gsumd  18372  evl1gsumadd  18373  zrhmulg  18525  chrval  18540  chrrhm  18546  znzrhval  18563  psgndiflemA  18615  ocvval  18676  elocv  18677  cssval  18691  pjfval  18715  pjfo  18724  isobs  18729  dsmmval  18743  dsmm0cl  18749  prdsinvgd2  18751  frlmvscaval  18778  frlmphl  18790  uvcval  18794  uvcvval  18795  uvcresum  18802  mat1dimscm  18955  mat1rhmelval  18960  marepvval  19047  mdetfval  19066  mdetleib2  19068  mdet0fv0  19074  m1detdiag  19077  mdetdiaglem  19078  mdetralt  19088  mdetunilem7  19098  mdetuni0  19101  m2detleiblem1  19104  smadiadetr  19155  cramerimplem1  19163  cpmatel  19190  1elcpmat  19194  cpmatinvcl  19196  cpmatmcllem  19197  cpmatmcl  19198  mat2pmatfval  19202  m2cpm  19220  cpm2mval  19229  cpm2mvalel  19230  m2cpminvid  19232  m2cpminvid2lem  19233  m2cpminvid2  19234  m2cpmfo  19235  decpmate  19245  decpmatid  19249  decpmatmullem  19250  decpmatmulsumfsupp  19252  monmatcollpw  19258  pmatcollpw3lem  19262  pmatcollpwscmatlem1  19268  pmatcollpwscmatlem2  19269  pm2mpf1  19278  pm2mpcoe1  19279  mply1topmatval  19283  mp2pm2mplem1  19285  mp2pm2mplem3  19287  mp2pm2mplem4  19288  mp2pm2mp  19290  pm2mpghm  19295  pm2mpmhmlem1  19297  pm2mpmhmlem2  19298  chpmatfval  19309  chpmat0d  19313  chpscmatgsumbin  19323  cayleyhamilton0  19368  cayleyhamiltonALT  19370  ntrval  19515  clsval  19516  opncldf3  19565  neival  19581  neiptopreu  19612  lpfval  19617  lpval  19618  cnpval  19715  iscnp2  19718  isreg  19811  isnrm  19814  2ndcsep  19938  isnlly  19948  ptval  20049  dfac14  20097  cnmptk2  20165  pt1hmeo  20285  xkocnv  20293  fmval  20422  ufldom  20441  flimval  20442  flffval  20468  flfval  20469  cnpflf  20480  txflf  20485  fclsval  20487  fcfval  20512  cnextval  20539  cnextfvval  20543  cnextcn  20545  cnextfres  20546  symgtgp  20578  tgpconcomp  20589  prdstmdd  20600  utopsnneiplem  20728  neipcfilu  20777  txmetcnp  21028  subgnm2  21126  tngngp  21146  isnlm  21162  sranlm  21171  lssnlm  21187  nmofval  21199  nmoval  21200  isphtpy  21459  pcovalg  21490  pco1  21493  clmneg  21559  clmabs  21560  nmoleub2lem3  21576  nmoleub3  21580  cphcjcl  21608  cphnm  21618  cphipcj  21624  cphassr  21636  tchnmval  21650  tchcphlem3  21654  ipcau2  21655  tchcphlem1  21656  tchcphlem2  21657  tchcph  21658  ipcau  21659  rrxnm  21801  rrxmval  21810  ovolctb  21879  voliunlem3  21940  uniioombllem2  21970  vitalilem4  21998  mbflimsup  22051  itg1climres  22099  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  mbfi1fseqlem6  22105  mbfi1flimlem  22107  mbfmullem2  22109  mbfmullem  22110  itg2monolem1  22135  itg2mono  22138  itg2i1fseqle  22139  itg2i1fseq  22140  itg2addlem  22143  itg2cnlem1  22146  limcfval  22254  limcmpt2  22266  limcres  22268  cnplimc  22269  dvfval  22279  dvreslem  22291  dvres2lem  22292  dvn0  22305  dvnp1  22306  cpnfval  22313  elcpn  22315  dvaddbr  22319  dvmulbr  22320  dvcmul  22325  dvfre  22332  rolle  22369  cmvth  22370  mvth  22371  dvlip  22372  dvlipcn  22373  dvlip2  22374  c1liplem1  22375  dveq0  22379  dv11cn  22380  dvivthlem1  22387  dvivth  22389  dvne0  22390  lhop1lem  22392  lhop2  22394  lhop  22395  dvcnvrelem2  22397  dvcvx  22399  dvfsumabs  22402  ftc1lem6  22420  ftc2  22423  ftc2ditglem  22424  itgparts  22426  itgsubstlem  22427  mdegaddle  22452  mdegmullem  22456  coe1mul3  22478  uc1pval  22518  mon1pval  22520  uc1pmon1p  22530  q1pval  22532  ply1remlem  22541  ply1rem  22542  fta1glem2  22545  fta1g  22546  fta1blem  22547  ig1pval  22551  plyeq0lem  22585  coeeulem  22599  coeid2  22614  dgrle  22618  dgreq  22619  0dgrb  22621  dgrnznn  22622  coemul  22627  coe11  22628  coe1term  22634  dgrlt  22641  dgradd2  22643  dgrcolem2  22649  plymul0or  22655  plydivlem4  22670  plydiveu  22672  plyremlem  22678  plyrem  22679  fta1  22682  vieta1lem2  22685  plyexmo  22687  aareccl  22700  aannenlem1  22702  aannenlem2  22703  taylfval  22732  tayl0  22735  dvtaylp  22743  dvntaylp0  22745  taylthlem1  22746  taylthlem2  22747  ulmval  22753  ulmres  22761  ulmshftlem  22762  ulmshft  22763  ulmuni  22765  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmdvlem1  22773  ulmdvlem3  22775  mtest  22777  mtestbdd  22778  mbfulm  22779  itgulm  22781  itgulm2  22782  pserval2  22784  pserulm  22795  psercn  22799  pserdvlem2  22801  pserdv  22802  pige3  22888  logtayl  23019  rlimcnp  23273  sqff1o  23434  muinv  23447  dchrinv  23514  sumdchr2  23523  dchr2sum  23526  lgsval4  23569  lgsmod  23574  lgsqrlem1  23594  dchrmusumlema  23656  dchrvmasumlem1  23658  dchrisum0re  23676  dchrisum0lema  23677  logsqvma2  23706  padicval  23780  istrkg2ld  23836  iscgrg  23882  midexlem  24047  israg  24052  colperpexlem2  24083  colperpexlem3  24084  opphllem  24087  midex  24089  mideu  24090  opphllem3  24099  midf  24120  ismidb  24122  lmieu  24128  lmimid  24137  brcgr  24181  ecgrtg  24264  wwlkn  24660  wlkiswwlkfun  24695  wlkiswwlkinj  24696  wlkiswwlksur  24697  wlkiswwlkbij2  24699  clwwlkn  24745  vdgrfval  24873  vdgrval  24874  isrgra  24904  isrgrac  24912  rusgranumwlklem4  24930  iseupa  24943  eupath2lem3  24957  eupath2  24958  vdfrgra0  25000  grpoinvval  25205  grpodivfval  25222  gxfval  25237  gxval  25238  imsdval  25570  sspnval  25628  nmoofval  25655  nmooval  25656  bloval  25674  0oval  25681  nmlno0  25688  hmoval  25703  ajval  25755  ubth  25767  htthlem  25812  pjhval  26293  pjoc1  26330  pjoc2  26335  pjige0  26587  pjcjt2  26588  pjch  26590  pjsumi  26606  pjdsi  26608  pjds3i  26609  pjopyth  26616  pjnorm  26620  pjpyth  26621  pjnel  26622  hosval  26637  homval  26638  hodval  26639  hfsval  26640  hfmval  26641  braval  26841  kbval  26851  eigvalval  26857  leopg  27019  leoppos  27023  leoprf2  27024  leoprf  27025  elpjrn  27087  pj3cor1i  27106  strlem2  27148  hstrlem2  27156  fmptcof2  27480  offval2f  27484  resf1o  27531  fpwrelmap  27534  fmcncfil  27891  nmmulg  27927  zrhnm  27928  qqhval  27933  qqhcn  27950  xrhval  27974  ofcfval  28075  ofcfval3  28079  brfae  28198  omsval  28242  sitgval  28252  eulerpartlemsv1  28273  eulerpartlemsf  28276  eulerpartlemgvv  28293  eulerpartlemn  28298  sseqval  28305  sseqfv1  28306  sseqfv2  28311  fibp1  28318  dstrvval  28387  ballotleme  28413  ballotlemi  28417  plymulx0  28482  plymulx  28483  signstfv  28498  signstfvneq0  28507  signstfvc  28509  signstres  28510  signstfveq0  28512  signsvvfval  28513  lgamgulmlem2  28550  lgamgulmlem5  28553  lgamgulm2  28556  lgamcvglem  28560  subfacp1lem5  28606  kur14  28638  ptpcon  28656  cvmliftmolem1  28704  cvmliftlem5  28712  cvmliftlem7  28714  cvmliftlem15  28721  cvmlift2lem3  28728  cvmlift2lem4  28729  cvmlift2lem7  28732  cvmlift2lem9  28734  cvmlift2  28739  cvmliftphtlem  28740  cvmlift3lem2  28743  cvmlift3lem5  28746  cvmlift3lem6  28747  cvmlift3lem7  28748  cvmlift3lem9  28750  cvmlift3  28751  mrsubfval  28846  msubffval  28861  msubfval  28862  mvhfval  28871  msubff1  28894  mclsval  28901  relexp0  29030  relexpsucr  29031  shftvalg  29093  bpolylem  29786  ftc2nc  30075  neibastop3  30156  tailval  30167  filnetlem4  30175  cocanfo  30184  f1ocan2fv  30194  upixp  30196  sdclem2  30211  rrncmslem  30304  ismrer1  30310  isnacs  30612  mzpsubst  30657  eldioph2  30671  pw2f1ocnv  30955  fnwe2lem2  30973  islnr3  31040  hbtlem1  31048  hbtlem2  31049  hbtlem7  31050  hbtlem4  31051  hbtlem5  31053  hbt  31055  dgrsub2  31060  mpaaeu  31075  mpaalem  31077  rgspnval  31093  flcidc  31099  cntzsdrg  31127  itgpowd  31158  addrfv  31332  subrfv  31333  mulvfv  31334  refsum2cnlem1  31366  n0p  31391  fvmpt2bd  31400  fmuldfeqlem1  31530  fmuldfeq  31531  fmul01lt1lem1  31532  fmul01lt1lem2  31533  limciccioolb  31581  limcicciooub  31597  cncfuni  31643  cncfiooicclem1  31650  dvsinax  31662  dvbdfbdioolem1  31679  dvnmptdivc  31689  dvnmul  31694  dvnprodlem1  31697  dvnprodlem2  31698  dvnprodlem3  31699  dvnprod  31700  itgsincmulx  31727  stoweidlem17  31753  stoweidlem20  31756  stoweidlem27  31763  stoweidlem31  31767  stoweidlem34  31770  stoweidlem44  31780  stoweidlem48  31784  stoweidlem59  31795  stirlinglem3  31812  stirlinglem15  31824  dirkeritg  31838  dirkercncflem2  31840  dirkercncflem3  31841  dirkercncflem4  31842  dirkercncf  31843  fourierdlem42  31885  fourierdlem60  31903  fourierdlem61  31904  fourierdlem68  31911  fourierdlem73  31916  fourierdlem80  31923  fourierdlem93  31936  fourierdlem94  31937  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem113  31956  elaa2lem  31970  elaa2  31971  etransclem17  31988  etransclem29  32000  etransclem32  32003  etransclem46  32017  funcestrcsetclem6  32617  funcsetcestrclem6  32632  rngcid  32662  ringcid  32705  funcringcsetcOLD2lem6  32721  funcringcsetclem6OLD  32744  coe1sclmulval  32855  ply1mulgsum  32860  evl1at0  32861  evl1at1  32862  lincvalpr  32889  bnj1379  33757  bj-finsumval0  34538  lshpset  34578  lsatset  34590  lkrval  34688  eqlkr  34699  ldualvaddval  34731  ldualvsval  34738  ldualvsubval  34757  cmtfvalN  34810  isoml  34838  pmapval  35356  pclvalN  35489  polfvalN  35503  polvalN  35504  psubclsetN  35535  watfvalN  35591  watvalN  35592  ldilset  35708  ltrnfset  35716  ltrnset  35717  dilfsetN  35752  dilsetN  35753  trnfsetN  35755  trnsetN  35756  trlfset  35760  trlset  35761  trlval  35762  ltrnideq  35775  cdlemd8  35805  cdlemg1idlemN  36173  cdlemg1fvawlemN  36174  cdlemg2idN  36197  trlcoabs2N  36323  tgrpfset  36345  tgrpset  36346  tendofset  36359  tendoset  36360  erngfset  36400  erngset  36401  erngfset-rN  36408  erngset-rN  36409  cdlemi2  36420  cdlemj1  36422  cdlemk2  36433  cdlemk4  36435  cdlemk8  36439  cdlemkuu  36496  cdlemk31  36497  cdlemkuv2-3N  36500  cdlemk18-3N  36501  cdlemk22-3  36502  cdlemkfid2N  36524  cdlemkyu  36528  cdlemk19ylem  36531  cdlemk46  36549  cdlemk49  36552  cdlemk43N  36564  cdlemk19u1  36570  cdlemk19u  36571  dvafset  36605  dvaset  36606  dvaplusgv  36611  diaffval  36632  diafval  36633  diaval  36634  dvhfset  36682  dvhset  36683  dvhlveclem  36710  docaffvalN  36723  docafvalN  36724  docavalN  36725  djaffvalN  36735  djafvalN  36736  dibffval  36742  dibfval  36743  dibval  36744  dicffval  36776  dicfval  36777  dicval  36778  dicelvalN  36780  dicvaddcl  36792  dicvscacl  36793  cdlemn8  36806  cdlemn9  36807  dihordlem7b  36817  dihffval  36832  dihfval  36833  dihval  36834  dihopelvalcpre  36850  dihmeetlem1N  36892  dihglblem5apreN  36893  dihmeetlem4preN  36908  dihmeetlem13N  36921  dih1dimatlem0  36930  dochffval  36951  dochfval  36952  dochval  36953  djhffval  36998  djhfval  36999  lcfl7lem  37101  lclkrlem2k  37119  lclkrlem2u  37129  lcdfval  37190  lcdval  37191  lcdvaddval  37200  lcdvsval  37206  lcd0vvalN  37215  lcdvsubval  37220  lcdlsp  37223  mapdffval  37228  mapdfval  37229  mapdval  37230  hvmapffval  37360  hvmapfval  37361  hvmapval  37362  hvmapvalvalN  37363  hvmapidN  37364  hvmaplkr  37370  hdmap1ffval  37398  hdmap1fval  37399  hdmap1vallem  37400  hdmapffval  37431  hdmapfval  37432  hdmapval  37433  hdmapevec2  37441  hgmapffval  37490  hgmapfval  37491  hgmapval  37492  hdmaplna2  37515  hdmapglnm2  37516  hdmapinvlem3  37525  hlhilset  37539  hlhilipval  37554
  Copyright terms: Public domain W3C validator