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

Theorem fveq1d 5689
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 5686 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ` cfv 5413
This theorem is referenced by:  fveq12d  5693  csbfv2g  5699  funssfv  5705  fvmptd  5769  fvmpt2d  5773  mpteqb  5778  fvmptt  5779  fmptco  5860  fvunsn  5884  fvsng  5886  fsnunfv  5892  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  fcofo  5980  ofval  6273  offval2  6281  ofrfval2  6282  caofinvl  6290  curry1val  6398  curry2val  6402  fnwelem  6420  rdg0g  6644  oav  6714  omv  6715  oev  6717  resixpfo  7059  pw2f1olem  7171  mapxpen  7232  xpmapenlem  7233  ordtypelem6  7448  ordtypelem7  7449  unwdomg  7508  cantnffval  7574  cantnfval  7579  cantnfres  7589  cantnfp1lem3  7592  fseqenlem1  7861  fseqenlem2  7862  iunfictbso  7951  dfac12lem1  7979  dfac12lem2  7980  dfac12r  7982  ackbij2lem3  8077  ituni0  8254  itunisuc  8255  itunitc1  8256  ituniiun  8258  hsmexlem2  8263  hsmexlem4  8265  iundom2g  8371  konigthlem  8399  konigth  8400  fpwwe2lem6  8466  fpwwe2lem9  8469  rpnnen1lem3  10558  rpnnen1lem5  10560  fseq1p1m1  11077  seqp1  11293  seqf1olem2  11318  seqf1o  11319  seqid  11323  seqz  11326  seqof  11335  seqof2  11336  bcval5  11564  bcn2  11565  hashf1lem1  11659  seqcoll  11667  s1fv  11715  swrdfv  11726  splfv1  11739  revfv  11750  shftcan1  11853  shftcan2  11854  climshft2  12331  isercoll2  12417  sumeq2w  12441  sumeq2ii  12442  cbvsum  12444  summo  12466  fsum  12469  fsumss  12474  fsumcvg2  12476  isumsplit  12575  rpnnen2lem1  12769  rpnnen2  12780  ruclem4  12788  sadfval  12919  smufval  12944  odzval  13132  1arithlem2  13247  vdwpc  13303  vdwlem6  13309  ramval  13331  setsid  13463  setsnid  13464  prdsval  13633  prdsplusgfval  13651  prdsmulrfval  13653  pwsvscaval  13672  imasval  13692  xpsc0  13740  xpsc1  13741  mrisval  13810  comfffval  13879  sectffval  13931  invinv  13950  oppcsect  13954  brssc  13969  issubc  13990  isfunc  14016  funcoppc  14027  idfuval  14028  idfu2  14030  idfu1  14032  idfucl  14033  cofuval  14034  cofu1  14036  cofu2  14038  cofuval2  14039  cofucl  14040  cofurid  14043  resfval  14044  resfval2  14045  funcres  14048  funcpropd  14052  isfull  14062  isnat  14099  fucco  14114  homafval  14139  idafval  14167  setcmon  14197  catcisolem  14216  catciso  14217  xpcval  14229  1stf1  14244  2ndf1  14247  1stfcl  14249  2ndfcl  14250  prfval  14251  prf2fval  14253  prf1st  14256  prf2nd  14257  1st2ndprf  14258  evlf2  14270  evlf2val  14271  evlfcl  14274  curfval  14275  curfpropd  14285  uncfval  14286  uncf2  14289  curfuncf  14290  diag11  14295  diag12  14296  diag2  14297  curf2ndf  14299  hofval  14304  hofcl  14311  yon11  14316  yon12  14317  yon2  14318  yonedalem4a  14327  yonedalem4b  14328  yonedalem4c  14329  yonedalem22  14330  yonedalem3b  14331  yonedainv  14333  yoniso  14337  lubval  14391  glbval  14396  joinfval  14399  meetfval  14406  isclat  14493  odumeet  14522  odujoin  14524  oduclatb  14526  poslubdg  14530  prdspjmhm  14721  pwsco1mhm  14724  gsumvalx  14729  gsumpropd  14731  gsumress  14732  gsumval2a  14737  grpsubfval  14802  grplactval  14841  grpsubpropd  14844  grpsubpropd2  14845  mulgfval  14846  mulgpropd  14878  submmulg  14880  pwsinvg  14885  subgmulg  14913  eqgfval  14943  lactghmga  15062  symgga  15064  cntrval  15073  cntzval  15075  cntzrcl  15081  oppgsubg  15114  ispgp  15181  vrgpval  15354  frgpup3lem  15364  frgpnabllem1  15439  frgpnabllem2  15440  gsumval3eu  15468  gsumval3  15469  gsumzres  15472  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  dmdprd  15514  dprdval  15516  dmdprdsplitlem  15550  dprd2da  15555  dpjfval  15568  dpjidcl  15571  dpjlid  15574  dpjrid  15575  dvrfval  15744  staffval  15890  srngnvl  15899  issrngd  15904  lspval  16006  islbs  16103  lbspropd  16126  lssacsex  16171  lbsacsbs  16183  sralem  16204  srasca  16208  sravsca  16209  rlmval  16219  lpival  16271  aspval  16342  psrmulval  16405  psrvscaval  16411  psrdi  16425  psrdir  16426  mvrval  16440  mvrval2  16441  mvrf1  16444  mplsubglem  16453  mplvscaval  16466  subrgmvrf  16480  opsrle  16491  opsrbaslem  16493  subrgasclcl  16514  psr1val  16539  vr1val  16545  coe1fv  16559  subrgvr1  16609  coe1addfv  16613  coe1subfv  16614  coe1tmfv1  16621  coe1tmfv2  16622  coe1tmmul2fv  16625  coe1pwmulfv  16627  coe1sclmulfv  16630  ply1sclid  16634  ply1sclf1  16635  zrhmulg  16746  chrval  16761  chrrhm  16767  znzrhval  16782  ocvval  16849  elocv  16850  cssval  16864  pjfval  16888  pjfo  16897  isobs  16902  ntrval  17055  clsval  17056  opncldf3  17105  neival  17121  neiptopreu  17152  lpfval  17157  lpval  17158  cnpval  17254  iscnp2  17257  isreg  17350  isnrm  17353  2ndcsep  17475  isnlly  17485  ptval  17555  dfac14  17603  cnmptk2  17671  pt1hmeo  17791  xkocnv  17799  fmval  17928  ufldom  17947  flimval  17948  flffval  17974  flfval  17975  cnpflf  17986  txflf  17991  fclsval  17993  fcfval  18018  cnextval  18045  cnextfvval  18049  cnextcn  18051  cnextfres  18052  symgtgp  18084  tgpconcomp  18095  prdstmdd  18106  utopsnneiplem  18230  neipcfilu  18279  txmetcnp  18530  subgnm2  18628  tngngp  18648  isnlm  18664  sranlm  18673  lssnlm  18689  nmofval  18701  nmoval  18702  isphtpy  18959  pcovalg  18990  pco1  18993  clmneg  19059  clmabs  19060  nmoleub2lem3  19076  nmoleub3  19080  cphcjcl  19099  cphnm  19109  cphipcj  19115  cphassr  19127  tchnmval  19140  tchcphlem3  19143  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  tchcph  19147  ipcau  19148  ovolctb  19339  voliunlem3  19399  uniioombllem2  19428  vitalilem4  19456  mbflimsup  19511  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfmullem2  19569  mbfmullem  19570  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2cnlem1  19606  limcfval  19712  limcmpt2  19724  limcres  19726  cnplimc  19727  dvfval  19737  dvreslem  19749  dvres2lem  19750  dvn0  19763  dvnp1  19764  cpnfval  19771  elcpn  19773  dvaddbr  19777  dvmulbr  19778  dvcmul  19783  dvfre  19790  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dveq0  19837  dv11cn  19838  dvivthlem1  19845  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem2  19855  dvcvx  19857  dvfsumabs  19860  ftc1lem6  19878  ftc2  19881  ftc2ditglem  19882  itgparts  19884  itgsubstlem  19885  evlslem1  19889  evlsval  19893  evlssca  19896  evlsvar  19897  evlval  19898  evl1sca  19903  evl1scad  19904  evl1var  19905  evl1vard  19906  evl1addd  19907  evl1subd  19908  evl1muld  19909  evl1vsd  19910  evl1expd  19911  pf1ind  19928  mdegaddle  19950  mdegmullem  19954  coe1mul3  19975  uc1pval  20015  mon1pval  20017  uc1pmon1p  20027  q1pval  20029  ply1remlem  20038  ply1rem  20039  fta1glem2  20042  fta1g  20043  fta1blem  20044  ig1pval  20048  plyeq0lem  20082  coeeulem  20096  coeid2  20111  dgrle  20115  dgreq  20116  0dgrb  20118  coemul  20123  coe11  20124  coe1term  20130  dgrlt  20137  dgradd2  20139  dgrcolem2  20145  plymul0or  20151  plydivlem4  20166  plydiveu  20168  plyremlem  20174  plyrem  20175  fta1  20178  vieta1lem2  20181  plyexmo  20183  aareccl  20196  aannenlem1  20198  aannenlem2  20199  taylfval  20228  tayl0  20231  dvtaylp  20239  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmval  20249  ulmres  20257  ulmshftlem  20258  ulmshft  20259  ulmuni  20261  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  mtestbdd  20274  mbfulm  20275  itgulm  20277  itgulm2  20278  pserval2  20280  pserulm  20291  psercn  20295  pserdvlem2  20297  pserdv  20298  pige3  20378  logtayl  20504  rlimcnp  20757  sqff1o  20918  muinv  20931  dchrinv  20998  sumdchr2  21007  dchr2sum  21010  lgsval4  21053  lgsmod  21058  lgsqrlem1  21078  dchrmusumlema  21140  dchrvmasumlem1  21142  dchrisum0re  21160  dchrisum0lema  21161  logsqvma2  21190  padicval  21264  vdgrfval  21619  vdgrval  21620  iseupa  21640  eupath2lem3  21654  eupath2  21655  grpoinvval  21766  grpodivfval  21783  gxfval  21798  gxval  21799  imsdval  22131  sspnval  22189  nmoofval  22216  nmooval  22217  bloval  22235  0oval  22242  nmlno0  22249  hmoval  22264  ajval  22316  ubth  22328  htthlem  22373  pjhval  22852  pjoc1  22889  pjoc2  22894  pjige0  23146  pjcjt2  23147  pjch  23149  pjsumi  23165  pjdsi  23167  pjds3i  23168  pjopyth  23175  pjnorm  23179  pjpyth  23180  pjnel  23181  hosval  23196  homval  23197  hodval  23198  hfsval  23199  hfmval  23200  braval  23400  kbval  23410  eigvalval  23416  leopg  23578  leoppos  23582  leoprf2  23583  leoprf  23584  elpjrn  23646  pj3cor1i  23665  strlem2  23707  hstrlem2  23715  fmptcof2  24029  offval2f  24033  fmcncfil  24270  nmmulg  24305  zrhnm  24306  qqhval  24311  qqhcn  24328  ofcfval  24434  ofcfval3  24438  brfae  24552  sitgval  24600  dstrvval  24681  ballotleme  24707  ballotlemi  24711  lgamgulmlem2  24767  lgamgulmlem5  24770  lgamgulm2  24773  lgamcvglem  24777  subfacp1lem5  24823  kur14  24855  ptpcon  24873  cvmliftmolem1  24921  cvmliftlem5  24929  cvmliftlem7  24931  cvmliftlem15  24938  cvmlift2lem3  24945  cvmlift2lem4  24946  cvmlift2lem7  24949  cvmlift2lem9  24951  cvmlift2  24956  cvmliftphtlem  24957  cvmlift3lem2  24960  cvmlift3lem5  24963  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  cvmlift3  24968  relexp0  25082  relexpsucr  25083  shftvalg  25161  prodeq2w  25191  prodeq2ii  25192  prodmo  25215  fprod  25220  fprodss  25227  brcgr  25743  bpolylem  25998  neibastop3  26281  tailval  26292  filnetlem4  26300  cocanfo  26309  f1ocan2fv  26319  upixp  26321  sdclem2  26336  rrncmslem  26431  ismrer1  26437  isnacs  26648  mzpsubst  26695  eldioph2  26710  pw2f1ocnv  26998  fnwe2lem2  27016  dsmmval  27068  dsmm0cl  27074  prdsinvgd2  27076  frlmvscaval  27099  uvcval  27102  uvcvval  27103  uvcresum  27110  islnr3  27187  hbtlem1  27195  hbtlem2  27196  hbtlem7  27197  hbtlem4  27198  hbtlem5  27200  hbt  27202  dgrsub2  27207  dgrnznn  27208  mpaaeu  27223  mpaalem  27225  rgspnval  27241  flcidc  27247  pmtrval  27262  pmtrfv  27263  pmtrffv  27269  mdetfval  27355  cntzsdrg  27378  addrfv  27541  subrfv  27542  mulvfv  27543  refsum2cnlem1  27575  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  stoweidlem17  27633  stoweidlem20  27636  stoweidlem27  27643  stoweidlem31  27647  stoweidlem34  27650  stoweidlem42  27658  stoweidlem44  27660  stoweidlem48  27664  stoweidlem59  27675  stirlinglem3  27692  stirlinglem15  27704  swrdswrd  28011  vdfrgra0  28126  vdgfrgra0  28127  bnj1379  28908  lshpset  29461  lsatset  29473  lkrval  29571  eqlkr  29582  ldualvaddval  29614  ldualvsval  29621  ldualvsubval  29640  cmtfvalN  29693  isoml  29721  pmapval  30239  pclvalN  30372  polfvalN  30386  polvalN  30387  psubclsetN  30418  watfvalN  30474  watvalN  30475  ldilset  30591  ltrnfset  30599  ltrnset  30600  dilfsetN  30634  dilsetN  30635  trnfsetN  30637  trnsetN  30638  trlfset  30642  trlset  30643  trlval  30644  ltrnideq  30657  cdlemd8  30687  cdlemg1idlemN  31054  cdlemg1fvawlemN  31055  cdlemg2idN  31078  trlcoabs2N  31204  tgrpfset  31226  tgrpset  31227  tendofset  31240  tendoset  31241  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  cdlemi2  31301  cdlemj1  31303  cdlemk2  31314  cdlemk4  31316  cdlemk8  31320  cdlemkuu  31377  cdlemk31  31378  cdlemkuv2-3N  31381  cdlemk18-3N  31382  cdlemk22-3  31383  cdlemkfid2N  31405  cdlemkyu  31409  cdlemk19ylem  31412  cdlemk46  31430  cdlemk49  31433  cdlemk43N  31445  cdlemk19u1  31451  cdlemk19u  31452  dvafset  31486  dvaset  31487  dvaplusgv  31492  diaffval  31513  diafval  31514  diaval  31515  dvhfset  31563  dvhset  31564  dvhlveclem  31591  docaffvalN  31604  docafvalN  31605  docavalN  31606  djaffvalN  31616  djafvalN  31617  dibffval  31623  dibfval  31624  dibval  31625  dicffval  31657  dicfval  31658  dicval  31659  dicelvalN  31661  dicvaddcl  31673  dicvscacl  31674  cdlemn8  31687  cdlemn9  31688  dihordlem7b  31698  dihffval  31713  dihfval  31714  dihval  31715  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem4preN  31789  dihmeetlem13N  31802  dih1dimatlem0  31811  dochffval  31832  dochfval  31833  dochval  31834  djhffval  31879  djhfval  31880  lcfl7lem  31982  lclkrlem2k  32000  lclkrlem2u  32010  lcdfval  32071  lcdval  32072  lcdvaddval  32081  lcdvsval  32087  lcd0vvalN  32096  lcdvsubval  32101  lcdlsp  32104  mapdffval  32109  mapdfval  32110  mapdval  32111  hvmapffval  32241  hvmapfval  32242  hvmapval  32243  hvmapvalvalN  32244  hvmapidN  32245  hvmaplkr  32251  hdmap1ffval  32279  hdmap1fval  32280  hdmap1vallem  32281  hdmapffval  32312  hdmapfval  32313  hdmapval  32314  hdmapevec2  32322  hgmapffval  32371  hgmapfval  32372  hgmapval  32373  hdmaplna2  32396  hdmapglnm2  32397  hdmapinvlem3  32406  hlhilset  32420  hlhilipval  32435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421
  Copyright terms: Public domain W3C validator