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

Theorem fveq1d 5529
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 5526 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 15 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625   ` cfv 5257
This theorem is referenced by:  fveq12d  5533  csbfv2g  5539  funssfv  5545  fvmptd  5608  mpteqb  5616  fvmptt  5617  fmptco  5693  fvunsn  5714  fvsng  5716  fsnunfv  5722  f1ocnvfv1  5794  f1ocnvfv2  5795  fcof1  5799  fcofo  5800  ofval  6089  offval2  6097  ofrfval2  6098  caofinvl  6106  curry1val  6213  curry2val  6217  fnwelem  6232  rdg0g  6442  oav  6512  omv  6513  oev  6515  resixpfo  6856  pw2f1olem  6968  mapxpen  7029  xpmapenlem  7030  ordtypelem6  7240  ordtypelem7  7241  unwdomg  7300  cantnffval  7366  cantnfval  7371  cantnfres  7381  cantnfp1lem3  7384  fseqenlem1  7653  fseqenlem2  7654  iunfictbso  7743  dfac12lem1  7771  dfac12lem2  7772  dfac12r  7774  ackbij2lem3  7869  ituni0  8046  itunisuc  8047  itunitc1  8048  ituniiun  8050  hsmexlem2  8055  hsmexlem4  8057  iundom2g  8164  konigthlem  8192  konigth  8193  fpwwe2lem6  8259  fpwwe2lem9  8262  rpnnen1lem3  10346  rpnnen1lem5  10348  fseq1p1m1  10859  seqp1  11063  seqf1olem2  11088  seqf1o  11089  seqid  11093  seqz  11096  seqof  11105  bcval5  11332  bcn2  11333  hashf1lem1  11395  seqcoll  11403  s1fv  11448  swrdfv  11459  splfv1  11472  revfv  11483  shftcan1  11580  shftcan2  11581  climshft2  12058  isercoll2  12144  sumeq2w  12167  sumeq2ii  12168  cbvsum  12170  summo  12192  fsum  12195  fsumss  12200  fsumcvg2  12202  isumsplit  12301  rpnnen2lem1  12495  rpnnen2  12506  ruclem4  12514  sadfval  12645  smufval  12670  odzval  12858  1arithlem2  12973  vdwpc  13029  vdwlem6  13035  ramval  13057  setsid  13189  setsnid  13190  prdsval  13357  prdsplusgfval  13375  prdsmulrfval  13377  pwsvscaval  13396  imasval  13416  xpsc0  13464  xpsc1  13465  mrisval  13534  comfffval  13603  sectffval  13655  invinv  13674  oppcsect  13678  brssc  13693  issubc  13714  isfunc  13740  funcoppc  13751  idfuval  13752  idfu2  13754  idfu1  13756  idfucl  13757  cofuval  13758  cofu1  13760  cofu2  13762  cofuval2  13763  cofucl  13764  cofurid  13767  resfval  13768  resfval2  13769  funcres  13772  funcpropd  13776  isfull  13786  isnat  13823  fucco  13838  homafval  13863  idafval  13891  setcmon  13921  catcisolem  13940  catciso  13941  xpcval  13953  1stf1  13968  2ndf1  13971  1stfcl  13973  2ndfcl  13974  prfval  13975  prf2fval  13977  prf1st  13980  prf2nd  13981  1st2ndprf  13982  evlf2  13994  evlf2val  13995  evlfcl  13998  curfval  13999  curfpropd  14009  uncfval  14010  uncf2  14013  curfuncf  14014  diag11  14019  diag12  14020  diag2  14021  curf2ndf  14023  hofval  14028  hofcl  14035  yon11  14040  yon12  14041  yon2  14042  yonedalem4a  14051  yonedalem4b  14052  yonedalem4c  14053  yonedalem22  14054  yonedalem3b  14055  yonedainv  14057  yoniso  14061  lubval  14115  glbval  14120  joinfval  14123  meetfval  14130  isclat  14217  odumeet  14246  odujoin  14248  oduclatb  14250  poslubdg  14254  prdspjmhm  14445  pwsco1mhm  14448  gsumvalx  14453  gsumpropd  14455  gsumress  14456  gsumval2a  14461  grpsubfval  14526  grplactval  14565  grpsubpropd  14568  grpsubpropd2  14569  mulgfval  14570  mulgpropd  14602  submmulg  14604  pwsinvg  14609  subgmulg  14637  eqgfval  14667  lactghmga  14786  symgga  14788  cntrval  14797  cntzval  14799  cntzrcl  14805  oppgsubg  14838  ispgp  14905  vrgpval  15078  frgpup3lem  15088  frgpnabllem1  15163  frgpnabllem2  15164  gsumval3eu  15192  gsumval3  15193  gsumzres  15196  gsumzf1o  15198  gsumzaddlem  15205  gsumconst  15211  dmdprd  15238  dprdval  15240  dmdprdsplitlem  15274  dprd2da  15279  dpjfval  15292  dpjidcl  15295  dpjlid  15298  dpjrid  15299  dvrfval  15468  staffval  15614  srngnvl  15623  issrngd  15628  lspval  15734  islbs  15831  lbspropd  15854  lssacsex  15899  lbsacsbs  15911  sralem  15932  srasca  15936  sravsca  15937  rlmval  15947  lpival  15999  aspval  16070  psrmulval  16133  psrvscaval  16139  psrdi  16153  psrdir  16154  mvrval  16168  mvrval2  16169  mvrf1  16172  mplsubglem  16181  mplvscaval  16194  subrgmvrf  16208  opsrle  16219  opsrbaslem  16221  subrgasclcl  16242  psr1val  16267  vr1val  16273  coe1fv  16289  subrgvr1  16340  coe1addfv  16344  coe1subfv  16345  coe1tmfv1  16352  coe1tmfv2  16353  coe1tmmul2fv  16356  coe1pwmulfv  16358  coe1sclmulfv  16361  ply1sclid  16365  ply1sclf1  16366  zrhmulg  16466  chrval  16481  chrrhm  16487  znzrhval  16502  ocvval  16569  elocv  16570  cssval  16584  pjfval  16608  pjfo  16617  isobs  16622  ntrval  16775  clsval  16776  opncldf3  16825  neival  16841  lpfval  16872  lpval  16873  cnpval  16968  iscnp2  16971  isreg  17062  isnrm  17065  2ndcsep  17187  isnlly  17197  ptval  17267  dfac14  17314  cnmptk2  17382  pt1hmeo  17499  xkocnv  17507  fmval  17640  ufldom  17659  flimval  17660  flffval  17686  flfval  17687  cnpflf  17698  txflf  17703  fclsval  17705  fcfval  17730  symgtgp  17786  tgpconcomp  17797  prdstmdd  17808  txmetcnp  18095  subgnm2  18152  tngngp  18172  isnlm  18188  sranlm  18197  lssnlm  18213  nmofval  18225  nmoval  18226  isphtpy  18481  pcovalg  18512  pco1  18515  clmneg  18581  clmabs  18582  nmoleub2lem3  18598  nmoleub3  18602  cphcjcl  18621  cphnm  18631  cphipcj  18637  cphassr  18649  tchnmval  18662  tchcphlem3  18665  ipcau2  18666  tchcphlem1  18667  tchcphlem2  18668  tchcph  18669  ipcau  18670  ovolctb  18851  voliunlem3  18911  uniioombllem2  18940  vitalilem4  18968  mbflimsup  19023  itg1climres  19071  mbfi1fseqlem4  19075  mbfi1fseqlem5  19076  mbfi1fseqlem6  19077  mbfi1flimlem  19079  mbfmullem2  19081  mbfmullem  19082  itg2monolem1  19107  itg2mono  19110  itg2i1fseqle  19111  itg2i1fseq  19112  itg2addlem  19115  itg2cnlem1  19118  limcfval  19224  limcmpt2  19236  limcres  19238  cnplimc  19239  dvfval  19249  dvreslem  19261  dvres2lem  19262  dvn0  19275  dvnp1  19276  cpnfval  19283  elcpn  19285  dvaddbr  19289  dvmulbr  19290  dvcmul  19295  dvfre  19302  rolle  19339  cmvth  19340  mvth  19341  dvlip  19342  dvlipcn  19343  dvlip2  19344  c1liplem1  19345  dveq0  19349  dv11cn  19350  dvivthlem1  19357  dvivth  19359  dvne0  19360  lhop1lem  19362  lhop2  19364  lhop  19365  dvcnvrelem2  19367  dvcvx  19369  dvfsumabs  19372  ftc1lem6  19390  ftc2  19393  ftc2ditglem  19394  itgparts  19396  itgsubstlem  19397  evlslem1  19401  evlsval  19405  evlssca  19408  evlsvar  19409  evlval  19410  evl1sca  19415  evl1scad  19416  evl1var  19417  evl1vard  19418  evl1addd  19419  evl1subd  19420  evl1muld  19421  evl1vsd  19422  evl1expd  19423  pf1ind  19440  mdegaddle  19462  mdegmullem  19466  coe1mul3  19487  uc1pval  19527  mon1pval  19529  uc1pmon1p  19539  q1pval  19541  ply1remlem  19550  ply1rem  19551  fta1glem2  19554  fta1g  19555  fta1blem  19556  ig1pval  19560  plyeq0lem  19594  coeeulem  19608  coeid2  19623  dgrle  19627  dgreq  19628  0dgrb  19630  coemul  19635  coe11  19636  coe1term  19642  dgrlt  19649  dgradd2  19651  dgrcolem2  19657  plymul0or  19663  plydivlem4  19678  plydiveu  19680  plyremlem  19686  plyrem  19687  fta1  19690  vieta1lem2  19693  plyexmo  19695  aareccl  19708  aannenlem1  19710  aannenlem2  19711  taylfval  19740  tayl0  19743  dvtaylp  19751  dvntaylp0  19753  taylthlem1  19754  taylthlem2  19755  ulmval  19761  ulmres  19769  ulmshftlem  19770  ulmshft  19771  ulmcaulem  19773  ulmcau  19774  ulmss  19776  ulmdvlem1  19779  ulmdvlem3  19781  mtest  19783  mbfulm  19784  itgulm  19786  itgulm2  19787  pserval2  19789  pserulm  19800  psercn  19804  pserdvlem2  19806  pserdv  19807  pige3  19887  logtayl  20009  rlimcnp  20262  sqff1o  20422  muinv  20435  dchrinv  20502  sumdchr2  20511  dchr2sum  20514  lgsval4  20557  lgsmod  20562  lgsqrlem1  20582  dchrmusumlema  20644  dchrvmasumlem1  20646  dchrisum0re  20664  dchrisum0lema  20665  logsqvma2  20694  padicval  20768  grpoinvval  20894  grpodivfval  20911  gxfval  20926  gxval  20927  imsdval  21257  sspnval  21315  nmoofval  21342  nmooval  21343  bloval  21361  0oval  21368  nmlno0  21375  hmoval  21390  ajval  21442  ubth  21454  htthlem  21499  pjhval  21978  pjoc1  22015  pjoc2  22020  pjige0  22272  pjcjt2  22273  pjch  22275  pjsumi  22291  pjdsi  22293  pjds3i  22294  pjopyth  22301  pjnorm  22305  pjpyth  22306  pjnel  22307  hosval  22322  homval  22323  hodval  22324  hfsval  22325  hfmval  22326  braval  22526  kbval  22536  eigvalval  22542  leopg  22704  leoppos  22708  leoprf2  22709  leoprf  22710  elpjrn  22772  pj3cor1i  22791  strlem2  22833  hstrlem2  22841  ballotleme  23057  ballotlemi  23061  fvmpt2d  23227  fmptcof2  23231  offval2f  23235  ofcfval  23461  ofcfval3  23465  itgmeq123dTMP  23591  dstrvval  23673  subfacp1lem5  23717  kur14  23749  ptpcon  23766  cvmliftmolem1  23814  cvmliftlem5  23822  cvmliftlem7  23824  cvmliftlem15  23831  cvmlift2lem3  23838  cvmlift2lem4  23839  cvmlift2lem7  23842  cvmlift2lem9  23844  cvmlift2  23849  cvmliftphtlem  23850  cvmlift3lem2  23853  cvmlift3lem5  23856  cvmlift3lem6  23857  cvmlift3lem7  23858  cvmlift3lem9  23860  cvmlift3  23861  iseupa  23883  vdgrfval  23891  vdgrval  23892  eupath2lem3  23905  eupath2  23906  relexp0  24027  relexpsucr  24028  brcgr  24530  bpolylem  24785  itg2addnclem  24933  itg2addnc  24935  valpr  25169  prjmapcp2  25181  valcurfn1  25215  valvalcurfn  25217  prodeq2  25318  dffprod  25330  fprodser  25331  islimrs  25591  valvze  25665  isucv  25688  mulmulvec  25698  distmlva  25699  distsava  25700  isder  25718  ishoma  25798  ishomd  25801  ismona  25820  isepia  25830  isiso  25836  cinvlem1  25839  isfuna  25845  isinob  25873  issrc  25878  propsrc  25879  isntr  25884  islimcat  25887  vtare  25896  vtarsu  25897  vtarl  25898  trclval  25905  isgraphmrph  25934  domcatfun  25936  domcatval  25941  codcatfun  25945  codcatval  25947  idmor  25957  cmp2morpdom  25975  isside0  26175  aishp  26183  isibcg  26202  neibastop3  26322  tailval  26333  filnetlem4  26341  cocanfo  26385  f1ocan2fv  26406  upixp  26414  sdclem2  26463  rrncmslem  26567  ismrer1  26573  isnacs  26790  mzpsubst  26837  eldioph2  26852  pw2f1ocnv  27141  fnwe2lem2  27159  dsmmval  27211  dsmm0cl  27217  prdsinvgd2  27219  frlmvscaval  27242  uvcval  27245  uvcvval  27246  uvcresum  27253  islnr3  27330  hbtlem1  27338  hbtlem2  27339  hbtlem7  27340  hbtlem4  27341  hbtlem5  27343  hbt  27345  dgrsub2  27350  dgrnznn  27351  mpaaeu  27366  mpaalem  27368  rgspnval  27384  flcidc  27390  pmtrval  27405  pmtrfv  27406  pmtrffv  27412  mdetfval  27498  cntzsdrg  27521  addrfv  27685  subrfv  27686  mulvfv  27687  refsum2cnlem1  27719  fmuldfeqlem1  27723  fmuldfeq  27724  fmul01lt1lem1  27725  fmul01lt1lem2  27726  stoweidlem17  27777  stoweidlem20  27780  stoweidlem27  27787  stoweidlem31  27791  stoweidlem34  27794  stoweidlem42  27802  stoweidlem44  27804  stoweidlem48  27808  stoweidlem59  27819  stirlinglem3  27836  stirlinglem15  27848  bnj1379  28936  lshpset  29241  lsatset  29253  lkrval  29351  eqlkr  29362  ldualvaddval  29394  ldualvsval  29401  ldualvsubval  29420  cmtfvalN  29473  isoml  29501  pmapval  30019  pclvalN  30152  polfvalN  30166  polvalN  30167  psubclsetN  30198  watfvalN  30254  watvalN  30255  ldilset  30371  ltrnfset  30379  ltrnset  30380  dilfsetN  30414  dilsetN  30415  trnfsetN  30417  trnsetN  30418  trlfset  30422  trlset  30423  trlval  30424  ltrnideq  30437  cdlemd8  30467  cdlemg1idlemN  30834  cdlemg1fvawlemN  30835  cdlemg2idN  30858  trlcoabs2N  30984  tgrpfset  31006  tgrpset  31007  tendofset  31020  tendoset  31021  erngfset  31061  erngset  31062  erngfset-rN  31069  erngset-rN  31070  cdlemi2  31081  cdlemj1  31083  cdlemk2  31094  cdlemk4  31096  cdlemk8  31100  cdlemkuu  31157  cdlemk31  31158  cdlemkuv2-3N  31161  cdlemk18-3N  31162  cdlemk22-3  31163  cdlemkfid2N  31185  cdlemkyu  31189  cdlemk19ylem  31192  cdlemk46  31210  cdlemk49  31213  cdlemk43N  31225  cdlemk19u1  31231  cdlemk19u  31232  dvafset  31266  dvaset  31267  dvaplusgv  31272  diaffval  31293  diafval  31294  diaval  31295  dvhfset  31343  dvhset  31344  dvhlveclem  31371  docaffvalN  31384  docafvalN  31385  docavalN  31386  djaffvalN  31396  djafvalN  31397  dibffval  31403  dibfval  31404  dibval  31405  dicffval  31437  dicfval  31438  dicval  31439  dicelvalN  31441  dicvaddcl  31453  dicvscacl  31454  cdlemn8  31467  cdlemn9  31468  dihordlem7b  31478  dihffval  31493  dihfval  31494  dihval  31495  dihopelvalcpre  31511  dihmeetlem1N  31553  dihglblem5apreN  31554  dihmeetlem4preN  31569  dihmeetlem13N  31582  dih1dimatlem0  31591  dochffval  31612  dochfval  31613  dochval  31614  djhffval  31659  djhfval  31660  lcfl7lem  31762  lclkrlem2k  31780  lclkrlem2u  31790  lcdfval  31851  lcdval  31852  lcdvaddval  31861  lcdvsval  31867  lcd0vvalN  31876  lcdvsubval  31881  lcdlsp  31884  mapdffval  31889  mapdfval  31890  mapdval  31891  hvmapffval  32021  hvmapfval  32022  hvmapval  32023  hvmapvalvalN  32024  hvmapidN  32025  hvmaplkr  32031  hdmap1ffval  32059  hdmap1fval  32060  hdmap1vallem  32061  hdmapffval  32092  hdmapfval  32093  hdmapval  32094  hdmapevec2  32102  hgmapffval  32151  hgmapfval  32152  hgmapval  32153  hdmaplna2  32176  hdmapglnm2  32177  hdmapinvlem3  32186  hlhilset  32200  hlhilipval  32215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265
  Copyright terms: Public domain W3C validator