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

Theorem fveq1d 5543
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 5540 . 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 1632   ` cfv 5271
This theorem is referenced by:  fveq12d  5547  csbfv2g  5553  funssfv  5559  fvmptd  5622  mpteqb  5630  fvmptt  5631  fmptco  5707  fvunsn  5728  fvsng  5730  fsnunfv  5736  f1ocnvfv1  5808  f1ocnvfv2  5809  fcof1  5813  fcofo  5814  ofval  6103  offval2  6111  ofrfval2  6112  caofinvl  6120  curry1val  6227  curry2val  6231  fnwelem  6246  rdg0g  6456  oav  6526  omv  6527  oev  6529  resixpfo  6870  pw2f1olem  6982  mapxpen  7043  xpmapenlem  7044  ordtypelem6  7254  ordtypelem7  7255  unwdomg  7314  cantnffval  7380  cantnfval  7385  cantnfres  7395  cantnfp1lem3  7398  fseqenlem1  7667  fseqenlem2  7668  iunfictbso  7757  dfac12lem1  7785  dfac12lem2  7786  dfac12r  7788  ackbij2lem3  7883  ituni0  8060  itunisuc  8061  itunitc1  8062  ituniiun  8064  hsmexlem2  8069  hsmexlem4  8071  iundom2g  8178  konigthlem  8206  konigth  8207  fpwwe2lem6  8273  fpwwe2lem9  8276  rpnnen1lem3  10360  rpnnen1lem5  10362  fseq1p1m1  10873  seqp1  11077  seqf1olem2  11102  seqf1o  11103  seqid  11107  seqz  11110  seqof  11119  bcval5  11346  bcn2  11347  hashf1lem1  11409  seqcoll  11417  s1fv  11462  swrdfv  11473  splfv1  11486  revfv  11497  shftcan1  11594  shftcan2  11595  climshft2  12072  isercoll2  12158  sumeq2w  12181  sumeq2ii  12182  cbvsum  12184  summo  12206  fsum  12209  fsumss  12214  fsumcvg2  12216  isumsplit  12315  rpnnen2lem1  12509  rpnnen2  12520  ruclem4  12528  sadfval  12659  smufval  12684  odzval  12872  1arithlem2  12987  vdwpc  13043  vdwlem6  13049  ramval  13071  setsid  13203  setsnid  13204  prdsval  13371  prdsplusgfval  13389  prdsmulrfval  13391  pwsvscaval  13410  imasval  13430  xpsc0  13478  xpsc1  13479  mrisval  13548  comfffval  13617  sectffval  13669  invinv  13688  oppcsect  13692  brssc  13707  issubc  13728  isfunc  13754  funcoppc  13765  idfuval  13766  idfu2  13768  idfu1  13770  idfucl  13771  cofuval  13772  cofu1  13774  cofu2  13776  cofuval2  13777  cofucl  13778  cofurid  13781  resfval  13782  resfval2  13783  funcres  13786  funcpropd  13790  isfull  13800  isnat  13837  fucco  13852  homafval  13877  idafval  13905  setcmon  13935  catcisolem  13954  catciso  13955  xpcval  13967  1stf1  13982  2ndf1  13985  1stfcl  13987  2ndfcl  13988  prfval  13989  prf2fval  13991  prf1st  13994  prf2nd  13995  1st2ndprf  13996  evlf2  14008  evlf2val  14009  evlfcl  14012  curfval  14013  curfpropd  14023  uncfval  14024  uncf2  14027  curfuncf  14028  diag11  14033  diag12  14034  diag2  14035  curf2ndf  14037  hofval  14042  hofcl  14049  yon11  14054  yon12  14055  yon2  14056  yonedalem4a  14065  yonedalem4b  14066  yonedalem4c  14067  yonedalem22  14068  yonedalem3b  14069  yonedainv  14071  yoniso  14075  lubval  14129  glbval  14134  joinfval  14137  meetfval  14144  isclat  14231  odumeet  14260  odujoin  14262  oduclatb  14264  poslubdg  14268  prdspjmhm  14459  pwsco1mhm  14462  gsumvalx  14467  gsumpropd  14469  gsumress  14470  gsumval2a  14475  grpsubfval  14540  grplactval  14579  grpsubpropd  14582  grpsubpropd2  14583  mulgfval  14584  mulgpropd  14616  submmulg  14618  pwsinvg  14623  subgmulg  14651  eqgfval  14681  lactghmga  14800  symgga  14802  cntrval  14811  cntzval  14813  cntzrcl  14819  oppgsubg  14852  ispgp  14919  vrgpval  15092  frgpup3lem  15102  frgpnabllem1  15177  frgpnabllem2  15178  gsumval3eu  15206  gsumval3  15207  gsumzres  15210  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  dmdprd  15252  dprdval  15254  dmdprdsplitlem  15288  dprd2da  15293  dpjfval  15306  dpjidcl  15309  dpjlid  15312  dpjrid  15313  dvrfval  15482  staffval  15628  srngnvl  15637  issrngd  15642  lspval  15748  islbs  15845  lbspropd  15868  lssacsex  15913  lbsacsbs  15925  sralem  15946  srasca  15950  sravsca  15951  rlmval  15961  lpival  16013  aspval  16084  psrmulval  16147  psrvscaval  16153  psrdi  16167  psrdir  16168  mvrval  16182  mvrval2  16183  mvrf1  16186  mplsubglem  16195  mplvscaval  16208  subrgmvrf  16222  opsrle  16233  opsrbaslem  16235  subrgasclcl  16256  psr1val  16281  vr1val  16287  coe1fv  16303  subrgvr1  16354  coe1addfv  16358  coe1subfv  16359  coe1tmfv1  16366  coe1tmfv2  16367  coe1tmmul2fv  16370  coe1pwmulfv  16372  coe1sclmulfv  16375  ply1sclid  16379  ply1sclf1  16380  zrhmulg  16480  chrval  16495  chrrhm  16501  znzrhval  16516  ocvval  16583  elocv  16584  cssval  16598  pjfval  16622  pjfo  16631  isobs  16636  ntrval  16789  clsval  16790  opncldf3  16839  neival  16855  lpfval  16886  lpval  16887  cnpval  16982  iscnp2  16985  isreg  17076  isnrm  17079  2ndcsep  17201  isnlly  17211  ptval  17281  dfac14  17328  cnmptk2  17396  pt1hmeo  17513  xkocnv  17521  fmval  17654  ufldom  17673  flimval  17674  flffval  17700  flfval  17701  cnpflf  17712  txflf  17717  fclsval  17719  fcfval  17744  symgtgp  17800  tgpconcomp  17811  prdstmdd  17822  txmetcnp  18109  subgnm2  18166  tngngp  18186  isnlm  18202  sranlm  18211  lssnlm  18227  nmofval  18239  nmoval  18240  isphtpy  18495  pcovalg  18526  pco1  18529  clmneg  18595  clmabs  18596  nmoleub2lem3  18612  nmoleub3  18616  cphcjcl  18635  cphnm  18645  cphipcj  18651  cphassr  18663  tchnmval  18676  tchcphlem3  18679  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  tchcph  18683  ipcau  18684  ovolctb  18865  voliunlem3  18925  uniioombllem2  18954  vitalilem4  18982  mbflimsup  19037  itg1climres  19085  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfmullem2  19095  mbfmullem  19096  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2cnlem1  19132  limcfval  19238  limcmpt2  19250  limcres  19252  cnplimc  19253  dvfval  19263  dvreslem  19275  dvres2lem  19276  dvn0  19289  dvnp1  19290  cpnfval  19297  elcpn  19299  dvaddbr  19303  dvmulbr  19304  dvcmul  19309  dvfre  19316  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dveq0  19363  dv11cn  19364  dvivthlem1  19371  dvivth  19373  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvrelem2  19381  dvcvx  19383  dvfsumabs  19386  ftc1lem6  19404  ftc2  19407  ftc2ditglem  19408  itgparts  19410  itgsubstlem  19411  evlslem1  19415  evlsval  19419  evlssca  19422  evlsvar  19423  evlval  19424  evl1sca  19429  evl1scad  19430  evl1var  19431  evl1vard  19432  evl1addd  19433  evl1subd  19434  evl1muld  19435  evl1vsd  19436  evl1expd  19437  pf1ind  19454  mdegaddle  19476  mdegmullem  19480  coe1mul3  19501  uc1pval  19541  mon1pval  19543  uc1pmon1p  19553  q1pval  19555  ply1remlem  19564  ply1rem  19565  fta1glem2  19568  fta1g  19569  fta1blem  19570  ig1pval  19574  plyeq0lem  19608  coeeulem  19622  coeid2  19637  dgrle  19641  dgreq  19642  0dgrb  19644  coemul  19649  coe11  19650  coe1term  19656  dgrlt  19663  dgradd2  19665  dgrcolem2  19671  plymul0or  19677  plydivlem4  19692  plydiveu  19694  plyremlem  19700  plyrem  19701  fta1  19704  vieta1lem2  19707  plyexmo  19709  aareccl  19722  aannenlem1  19724  aannenlem2  19725  taylfval  19754  tayl0  19757  dvtaylp  19765  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmval  19775  ulmres  19783  ulmshftlem  19784  ulmshft  19785  ulmcaulem  19787  ulmcau  19788  ulmss  19790  ulmdvlem1  19793  ulmdvlem3  19795  mtest  19797  mbfulm  19798  itgulm  19800  itgulm2  19801  pserval2  19803  pserulm  19814  psercn  19818  pserdvlem2  19820  pserdv  19821  pige3  19901  logtayl  20023  rlimcnp  20276  sqff1o  20436  muinv  20449  dchrinv  20516  sumdchr2  20525  dchr2sum  20528  lgsval4  20571  lgsmod  20576  lgsqrlem1  20596  dchrmusumlema  20658  dchrvmasumlem1  20660  dchrisum0re  20678  dchrisum0lema  20679  logsqvma2  20708  padicval  20782  grpoinvval  20908  grpodivfval  20925  gxfval  20940  gxval  20941  imsdval  21271  sspnval  21329  nmoofval  21356  nmooval  21357  bloval  21375  0oval  21382  nmlno0  21389  hmoval  21404  ajval  21456  ubth  21468  htthlem  21513  pjhval  21992  pjoc1  22029  pjoc2  22034  pjige0  22286  pjcjt2  22287  pjch  22289  pjsumi  22305  pjdsi  22307  pjds3i  22308  pjopyth  22315  pjnorm  22319  pjpyth  22320  pjnel  22321  hosval  22336  homval  22337  hodval  22338  hfsval  22339  hfmval  22340  braval  22540  kbval  22550  eigvalval  22556  leopg  22718  leoppos  22722  leoprf2  22723  leoprf  22724  elpjrn  22786  pj3cor1i  22805  strlem2  22847  hstrlem2  22855  ballotleme  23071  ballotlemi  23075  fvmpt2d  23240  fmptcof2  23244  offval2f  23248  ofcfval  23474  ofcfval3  23478  itgmeq123dTMP  23604  dstrvval  23686  subfacp1lem5  23730  kur14  23762  ptpcon  23779  cvmliftmolem1  23827  cvmliftlem5  23835  cvmliftlem7  23837  cvmliftlem15  23844  cvmlift2lem3  23851  cvmlift2lem4  23852  cvmlift2lem7  23855  cvmlift2lem9  23857  cvmlift2  23862  cvmliftphtlem  23863  cvmlift3lem2  23866  cvmlift3lem5  23869  cvmlift3lem6  23870  cvmlift3lem7  23871  cvmlift3lem9  23873  cvmlift3  23874  iseupa  23896  vdgrfval  23904  vdgrval  23905  eupath2lem3  23918  eupath2  23919  relexp0  24040  relexpsucr  24041  cprodeq2w  24134  cprodeq2ii  24135  prodmo  24159  fprod  24164  brcgr  24600  bpolylem  24855  itg2addnclem  25003  itg2addnc  25005  valpr  25261  prjmapcp2  25273  valcurfn1  25307  valvalcurfn  25309  prodeq2  25410  dffprod  25422  fprodser  25423  islimrs  25683  valvze  25757  isucv  25780  mulmulvec  25790  distmlva  25791  distsava  25792  isder  25810  ishoma  25890  ishomd  25893  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  isfuna  25937  isinob  25965  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  vtare  25988  vtarsu  25989  vtarl  25990  trclval  25997  isgraphmrph  26026  domcatfun  26028  domcatval  26033  codcatfun  26037  codcatval  26039  idmor  26049  cmp2morpdom  26067  isside0  26267  aishp  26275  isibcg  26294  neibastop3  26414  tailval  26425  filnetlem4  26433  cocanfo  26477  f1ocan2fv  26498  upixp  26506  sdclem2  26555  rrncmslem  26659  ismrer1  26665  isnacs  26882  mzpsubst  26929  eldioph2  26944  pw2f1ocnv  27233  fnwe2lem2  27251  dsmmval  27303  dsmm0cl  27309  prdsinvgd2  27311  frlmvscaval  27334  uvcval  27337  uvcvval  27338  uvcresum  27345  islnr3  27422  hbtlem1  27430  hbtlem2  27431  hbtlem7  27432  hbtlem4  27433  hbtlem5  27435  hbt  27437  dgrsub2  27442  dgrnznn  27443  mpaaeu  27458  mpaalem  27460  rgspnval  27476  flcidc  27482  pmtrval  27497  pmtrfv  27498  pmtrffv  27504  mdetfval  27590  cntzsdrg  27613  addrfv  27777  subrfv  27778  mulvfv  27779  refsum2cnlem1  27811  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  stoweidlem17  27869  stoweidlem20  27872  stoweidlem27  27879  stoweidlem31  27883  stoweidlem34  27886  stoweidlem42  27894  stoweidlem44  27896  stoweidlem48  27900  stoweidlem59  27911  stirlinglem3  27928  stirlinglem15  27940  bnj1379  29179  lshpset  29790  lsatset  29802  lkrval  29900  eqlkr  29911  ldualvaddval  29943  ldualvsval  29950  ldualvsubval  29969  cmtfvalN  30022  isoml  30050  pmapval  30568  pclvalN  30701  polfvalN  30715  polvalN  30716  psubclsetN  30747  watfvalN  30803  watvalN  30804  ldilset  30920  ltrnfset  30928  ltrnset  30929  dilfsetN  30963  dilsetN  30964  trnfsetN  30966  trnsetN  30967  trlfset  30971  trlset  30972  trlval  30973  ltrnideq  30986  cdlemd8  31016  cdlemg1idlemN  31383  cdlemg1fvawlemN  31384  cdlemg2idN  31407  trlcoabs2N  31533  tgrpfset  31555  tgrpset  31556  tendofset  31569  tendoset  31570  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  cdlemi2  31630  cdlemj1  31632  cdlemk2  31643  cdlemk4  31645  cdlemk8  31649  cdlemkuu  31706  cdlemk31  31707  cdlemkuv2-3N  31710  cdlemk18-3N  31711  cdlemk22-3  31712  cdlemkfid2N  31734  cdlemkyu  31738  cdlemk19ylem  31741  cdlemk46  31759  cdlemk49  31762  cdlemk43N  31774  cdlemk19u1  31780  cdlemk19u  31781  dvafset  31815  dvaset  31816  dvaplusgv  31821  diaffval  31842  diafval  31843  diaval  31844  dvhfset  31892  dvhset  31893  dvhlveclem  31920  docaffvalN  31933  docafvalN  31934  docavalN  31935  djaffvalN  31945  djafvalN  31946  dibffval  31952  dibfval  31953  dibval  31954  dicffval  31986  dicfval  31987  dicval  31988  dicelvalN  31990  dicvaddcl  32002  dicvscacl  32003  cdlemn8  32016  cdlemn9  32017  dihordlem7b  32027  dihffval  32042  dihfval  32043  dihval  32044  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem4preN  32118  dihmeetlem13N  32131  dih1dimatlem0  32140  dochffval  32161  dochfval  32162  dochval  32163  djhffval  32208  djhfval  32209  lcfl7lem  32311  lclkrlem2k  32329  lclkrlem2u  32339  lcdfval  32400  lcdval  32401  lcdvaddval  32410  lcdvsval  32416  lcd0vvalN  32425  lcdvsubval  32430  lcdlsp  32433  mapdffval  32438  mapdfval  32439  mapdval  32440  hvmapffval  32570  hvmapfval  32571  hvmapval  32572  hvmapvalvalN  32573  hvmapidN  32574  hvmaplkr  32580  hdmap1ffval  32608  hdmap1fval  32609  hdmap1vallem  32610  hdmapffval  32641  hdmapfval  32642  hdmapval  32643  hdmapevec2  32651  hgmapffval  32700  hgmapfval  32701  hgmapval  32702  hdmaplna2  32725  hdmapglnm2  32726  hdmapinvlem3  32735  hlhilset  32749  hlhilipval  32764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator