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

Theorem fveq1d 5634
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 5631 . 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 1647   ` cfv 5358
This theorem is referenced by:  fveq12d  5638  csbfv2g  5644  funssfv  5650  fvmptd  5713  mpteqb  5721  fvmptt  5722  fmptco  5802  fvunsn  5825  fvsng  5827  fsnunfv  5833  f1ocnvfv1  5914  f1ocnvfv2  5915  fcof1  5920  fcofo  5921  ofval  6214  offval2  6222  ofrfval2  6223  caofinvl  6231  curry1val  6339  curry2val  6343  fnwelem  6358  rdg0g  6582  oav  6652  omv  6653  oev  6655  resixpfo  6997  pw2f1olem  7109  mapxpen  7170  xpmapenlem  7171  ordtypelem6  7385  ordtypelem7  7386  unwdomg  7445  cantnffval  7511  cantnfval  7516  cantnfres  7526  cantnfp1lem3  7529  fseqenlem1  7798  fseqenlem2  7799  iunfictbso  7888  dfac12lem1  7916  dfac12lem2  7917  dfac12r  7919  ackbij2lem3  8014  ituni0  8191  itunisuc  8192  itunitc1  8193  ituniiun  8195  hsmexlem2  8200  hsmexlem4  8202  iundom2g  8309  konigthlem  8337  konigth  8338  fpwwe2lem6  8404  fpwwe2lem9  8407  rpnnen1lem3  10495  rpnnen1lem5  10497  fseq1p1m1  11012  seqp1  11225  seqf1olem2  11250  seqf1o  11251  seqid  11255  seqz  11258  seqof  11267  seqof2  11268  bcval5  11496  bcn2  11497  hashf1lem1  11591  seqcoll  11599  s1fv  11647  swrdfv  11658  splfv1  11671  revfv  11682  shftcan1  11785  shftcan2  11786  climshft2  12263  isercoll2  12349  sumeq2w  12373  sumeq2ii  12374  cbvsum  12376  summo  12398  fsum  12401  fsumss  12406  fsumcvg2  12408  isumsplit  12507  rpnnen2lem1  12701  rpnnen2  12712  ruclem4  12720  sadfval  12851  smufval  12876  odzval  13064  1arithlem2  13179  vdwpc  13235  vdwlem6  13241  ramval  13263  setsid  13395  setsnid  13396  prdsval  13565  prdsplusgfval  13583  prdsmulrfval  13585  pwsvscaval  13604  imasval  13624  xpsc0  13672  xpsc1  13673  mrisval  13742  comfffval  13811  sectffval  13863  invinv  13882  oppcsect  13886  brssc  13901  issubc  13922  isfunc  13948  funcoppc  13959  idfuval  13960  idfu2  13962  idfu1  13964  idfucl  13965  cofuval  13966  cofu1  13968  cofu2  13970  cofuval2  13971  cofucl  13972  cofurid  13975  resfval  13976  resfval2  13977  funcres  13980  funcpropd  13984  isfull  13994  isnat  14031  fucco  14046  homafval  14071  idafval  14099  setcmon  14129  catcisolem  14148  catciso  14149  xpcval  14161  1stf1  14176  2ndf1  14179  1stfcl  14181  2ndfcl  14182  prfval  14183  prf2fval  14185  prf1st  14188  prf2nd  14189  1st2ndprf  14190  evlf2  14202  evlf2val  14203  evlfcl  14206  curfval  14207  curfpropd  14217  uncfval  14218  uncf2  14221  curfuncf  14222  diag11  14227  diag12  14228  diag2  14229  curf2ndf  14231  hofval  14236  hofcl  14243  yon11  14248  yon12  14249  yon2  14250  yonedalem4a  14259  yonedalem4b  14260  yonedalem4c  14261  yonedalem22  14262  yonedalem3b  14263  yonedainv  14265  yoniso  14269  lubval  14323  glbval  14328  joinfval  14331  meetfval  14338  isclat  14425  odumeet  14454  odujoin  14456  oduclatb  14458  poslubdg  14462  prdspjmhm  14653  pwsco1mhm  14656  gsumvalx  14661  gsumpropd  14663  gsumress  14664  gsumval2a  14669  grpsubfval  14734  grplactval  14773  grpsubpropd  14776  grpsubpropd2  14777  mulgfval  14778  mulgpropd  14810  submmulg  14812  pwsinvg  14817  subgmulg  14845  eqgfval  14875  lactghmga  14994  symgga  14996  cntrval  15005  cntzval  15007  cntzrcl  15013  oppgsubg  15046  ispgp  15113  vrgpval  15286  frgpup3lem  15296  frgpnabllem1  15371  frgpnabllem2  15372  gsumval3eu  15400  gsumval3  15401  gsumzres  15404  gsumzf1o  15406  gsumzaddlem  15413  gsumconst  15419  dmdprd  15446  dprdval  15448  dmdprdsplitlem  15482  dprd2da  15487  dpjfval  15500  dpjidcl  15503  dpjlid  15506  dpjrid  15507  dvrfval  15676  staffval  15822  srngnvl  15831  issrngd  15836  lspval  15942  islbs  16039  lbspropd  16062  lssacsex  16107  lbsacsbs  16119  sralem  16140  srasca  16144  sravsca  16145  rlmval  16155  lpival  16207  aspval  16278  psrmulval  16341  psrvscaval  16347  psrdi  16361  psrdir  16362  mvrval  16376  mvrval2  16377  mvrf1  16380  mplsubglem  16389  mplvscaval  16402  subrgmvrf  16416  opsrle  16427  opsrbaslem  16429  subrgasclcl  16450  psr1val  16475  vr1val  16481  coe1fv  16497  subrgvr1  16548  coe1addfv  16552  coe1subfv  16553  coe1tmfv1  16560  coe1tmfv2  16561  coe1tmmul2fv  16564  coe1pwmulfv  16566  coe1sclmulfv  16569  ply1sclid  16573  ply1sclf1  16574  zrhmulg  16681  chrval  16696  chrrhm  16702  znzrhval  16717  ocvval  16784  elocv  16785  cssval  16799  pjfval  16823  pjfo  16832  isobs  16837  ntrval  16990  clsval  16991  opncldf3  17040  neival  17056  lpfval  17087  lpval  17088  cnpval  17183  iscnp2  17186  isreg  17277  isnrm  17280  2ndcsep  17402  isnlly  17412  ptval  17482  dfac14  17529  cnmptk2  17597  pt1hmeo  17714  xkocnv  17722  fmval  17851  ufldom  17870  flimval  17871  flffval  17897  flfval  17898  cnpflf  17909  txflf  17914  fclsval  17916  fcfval  17941  symgtgp  17997  tgpconcomp  18008  prdstmdd  18019  txmetcnp  18306  subgnm2  18363  tngngp  18383  isnlm  18399  sranlm  18408  lssnlm  18424  nmofval  18436  nmoval  18437  isphtpy  18694  pcovalg  18725  pco1  18728  clmneg  18794  clmabs  18795  nmoleub2lem3  18811  nmoleub3  18815  cphcjcl  18834  cphnm  18844  cphipcj  18850  cphassr  18862  tchnmval  18875  tchcphlem3  18878  ipcau2  18879  tchcphlem1  18880  tchcphlem2  18881  tchcph  18882  ipcau  18883  ovolctb  19064  voliunlem3  19124  uniioombllem2  19153  vitalilem4  19181  mbflimsup  19236  itg1climres  19284  mbfi1fseqlem4  19288  mbfi1fseqlem5  19289  mbfi1fseqlem6  19290  mbfi1flimlem  19292  mbfmullem2  19294  mbfmullem  19295  itg2monolem1  19320  itg2mono  19323  itg2i1fseqle  19324  itg2i1fseq  19325  itg2addlem  19328  itg2cnlem1  19331  limcfval  19437  limcmpt2  19449  limcres  19451  cnplimc  19452  dvfval  19462  dvreslem  19474  dvres2lem  19475  dvn0  19488  dvnp1  19489  cpnfval  19496  elcpn  19498  dvaddbr  19502  dvmulbr  19503  dvcmul  19508  dvfre  19515  rolle  19552  cmvth  19553  mvth  19554  dvlip  19555  dvlipcn  19556  dvlip2  19557  c1liplem1  19558  dveq0  19562  dv11cn  19563  dvivthlem1  19570  dvivth  19572  dvne0  19573  lhop1lem  19575  lhop2  19577  lhop  19578  dvcnvrelem2  19580  dvcvx  19582  dvfsumabs  19585  ftc1lem6  19603  ftc2  19606  ftc2ditglem  19607  itgparts  19609  itgsubstlem  19610  evlslem1  19614  evlsval  19618  evlssca  19621  evlsvar  19622  evlval  19623  evl1sca  19628  evl1scad  19629  evl1var  19630  evl1vard  19631  evl1addd  19632  evl1subd  19633  evl1muld  19634  evl1vsd  19635  evl1expd  19636  pf1ind  19653  mdegaddle  19675  mdegmullem  19679  coe1mul3  19700  uc1pval  19740  mon1pval  19742  uc1pmon1p  19752  q1pval  19754  ply1remlem  19763  ply1rem  19764  fta1glem2  19767  fta1g  19768  fta1blem  19769  ig1pval  19773  plyeq0lem  19807  coeeulem  19821  coeid2  19836  dgrle  19840  dgreq  19841  0dgrb  19843  coemul  19848  coe11  19849  coe1term  19855  dgrlt  19862  dgradd2  19864  dgrcolem2  19870  plymul0or  19876  plydivlem4  19891  plydiveu  19893  plyremlem  19899  plyrem  19900  fta1  19903  vieta1lem2  19906  plyexmo  19908  aareccl  19921  aannenlem1  19923  aannenlem2  19924  taylfval  19953  tayl0  19956  dvtaylp  19964  dvntaylp0  19966  taylthlem1  19967  taylthlem2  19968  ulmval  19974  ulmres  19982  ulmshftlem  19983  ulmshft  19984  ulmuni  19986  ulmcaulem  19988  ulmcau  19989  ulmss  19991  ulmdvlem1  19994  ulmdvlem3  19996  mtest  19998  mtestbdd  19999  mbfulm  20000  itgulm  20002  itgulm2  20003  pserval2  20005  pserulm  20016  psercn  20020  pserdvlem2  20022  pserdv  20023  pige3  20103  logtayl  20229  rlimcnp  20482  sqff1o  20643  muinv  20656  dchrinv  20723  sumdchr2  20732  dchr2sum  20735  lgsval4  20778  lgsmod  20783  lgsqrlem1  20803  dchrmusumlema  20865  dchrvmasumlem1  20867  dchrisum0re  20885  dchrisum0lema  20886  logsqvma2  20915  padicval  20989  grpoinvval  21203  grpodivfval  21220  gxfval  21235  gxval  21236  imsdval  21568  sspnval  21626  nmoofval  21653  nmooval  21654  bloval  21672  0oval  21679  nmlno0  21686  hmoval  21701  ajval  21753  ubth  21765  htthlem  21810  pjhval  22289  pjoc1  22326  pjoc2  22331  pjige0  22583  pjcjt2  22584  pjch  22586  pjsumi  22602  pjdsi  22604  pjds3i  22605  pjopyth  22612  pjnorm  22616  pjpyth  22617  pjnel  22618  hosval  22633  homval  22634  hodval  22635  hfsval  22636  hfmval  22637  braval  22837  kbval  22847  eigvalval  22853  leopg  23015  leoppos  23019  leoprf2  23020  leoprf  23021  elpjrn  23083  pj3cor1i  23102  strlem2  23144  hstrlem2  23152  fvmpt2d  23475  fmptcof2  23479  offval2f  23483  neiptopreu  23645  cnextval  23697  cnextfvval  23701  cnextcn  23703  utopsnneiplem  23750  nmmulg  23826  zrhnm  23827  qqhcn  23847  ofcfval  23946  ofcfval3  23950  brfae  24062  dstrvval  24176  ballotleme  24202  ballotlemi  24206  lgamgulmlem2  24262  lgamgulmlem5  24265  lgamgulm2  24268  lgamcvglem  24272  subfacp1lem5  24318  kur14  24350  ptpcon  24367  cvmliftmolem1  24415  cvmliftlem5  24423  cvmliftlem7  24425  cvmliftlem15  24432  cvmlift2lem3  24439  cvmlift2lem4  24440  cvmlift2lem7  24443  cvmlift2lem9  24445  cvmlift2  24450  cvmliftphtlem  24451  cvmlift3lem2  24454  cvmlift3lem5  24457  cvmlift3lem6  24458  cvmlift3lem7  24459  cvmlift3lem9  24461  cvmlift3  24462  iseupa  24468  vdgrfval  24476  vdgrval  24477  eupath2lem3  24490  eupath2  24491  relexp0  24612  relexpsucr  24613  shftvalg  24692  prodeq2w  24722  prodeq2ii  24723  prodmo  24746  fprod  24751  fprodss  24758  brcgr  25270  bpolylem  25525  itg2addnclem  25675  itg2addnc  25677  neibastop3  25818  tailval  25829  filnetlem4  25837  cocanfo  25881  f1ocan2fv  25902  upixp  25910  sdclem2  25959  rrncmslem  26062  ismrer1  26068  isnacs  26285  mzpsubst  26332  eldioph2  26347  pw2f1ocnv  26636  fnwe2lem2  26654  dsmmval  26706  dsmm0cl  26712  prdsinvgd2  26714  frlmvscaval  26737  uvcval  26740  uvcvval  26741  uvcresum  26748  islnr3  26825  hbtlem1  26833  hbtlem2  26834  hbtlem7  26835  hbtlem4  26836  hbtlem5  26838  hbt  26840  dgrsub2  26845  dgrnznn  26846  mpaaeu  26861  mpaalem  26863  rgspnval  26879  flcidc  26885  pmtrval  26900  pmtrfv  26901  pmtrffv  26907  mdetfval  26993  cntzsdrg  27016  addrfv  27180  subrfv  27181  mulvfv  27182  refsum2cnlem1  27214  fmuldfeqlem1  27218  fmuldfeq  27219  fmul01lt1lem1  27220  fmul01lt1lem2  27221  stoweidlem17  27272  stoweidlem20  27275  stoweidlem27  27282  stoweidlem31  27286  stoweidlem34  27289  stoweidlem42  27297  stoweidlem44  27299  stoweidlem48  27303  stoweidlem59  27314  stirlinglem3  27331  stirlinglem15  27343  vdgrefval  27805  vdgreval  27806  vdfrgra0  27857  vdgfrgra0  27858  bnj1379  28627  lshpset  29239  lsatset  29251  lkrval  29349  eqlkr  29360  ldualvaddval  29392  ldualvsval  29399  ldualvsubval  29418  cmtfvalN  29471  isoml  29499  pmapval  30017  pclvalN  30150  polfvalN  30164  polvalN  30165  psubclsetN  30196  watfvalN  30252  watvalN  30253  ldilset  30369  ltrnfset  30377  ltrnset  30378  dilfsetN  30412  dilsetN  30413  trnfsetN  30415  trnsetN  30416  trlfset  30420  trlset  30421  trlval  30422  ltrnideq  30435  cdlemd8  30465  cdlemg1idlemN  30832  cdlemg1fvawlemN  30833  cdlemg2idN  30856  trlcoabs2N  30982  tgrpfset  31004  tgrpset  31005  tendofset  31018  tendoset  31019  erngfset  31059  erngset  31060  erngfset-rN  31067  erngset-rN  31068  cdlemi2  31079  cdlemj1  31081  cdlemk2  31092  cdlemk4  31094  cdlemk8  31098  cdlemkuu  31155  cdlemk31  31156  cdlemkuv2-3N  31159  cdlemk18-3N  31160  cdlemk22-3  31161  cdlemkfid2N  31183  cdlemkyu  31187  cdlemk19ylem  31190  cdlemk46  31208  cdlemk49  31211  cdlemk43N  31223  cdlemk19u1  31229  cdlemk19u  31230  dvafset  31264  dvaset  31265  dvaplusgv  31270  diaffval  31291  diafval  31292  diaval  31293  dvhfset  31341  dvhset  31342  dvhlveclem  31369  docaffvalN  31382  docafvalN  31383  docavalN  31384  djaffvalN  31394  djafvalN  31395  dibffval  31401  dibfval  31402  dibval  31403  dicffval  31435  dicfval  31436  dicval  31437  dicelvalN  31439  dicvaddcl  31451  dicvscacl  31452  cdlemn8  31465  cdlemn9  31466  dihordlem7b  31476  dihffval  31491  dihfval  31492  dihval  31493  dihopelvalcpre  31509  dihmeetlem1N  31551  dihglblem5apreN  31552  dihmeetlem4preN  31567  dihmeetlem13N  31580  dih1dimatlem0  31589  dochffval  31610  dochfval  31611  dochval  31612  djhffval  31657  djhfval  31658  lcfl7lem  31760  lclkrlem2k  31778  lclkrlem2u  31788  lcdfval  31849  lcdval  31850  lcdvaddval  31859  lcdvsval  31865  lcd0vvalN  31874  lcdvsubval  31879  lcdlsp  31882  mapdffval  31887  mapdfval  31888  mapdval  31889  hvmapffval  32019  hvmapfval  32020  hvmapval  32021  hvmapvalvalN  32022  hvmapidN  32023  hvmaplkr  32029  hdmap1ffval  32057  hdmap1fval  32058  hdmap1vallem  32059  hdmapffval  32090  hdmapfval  32091  hdmapval  32092  hdmapevec2  32100  hgmapffval  32149  hgmapfval  32150  hgmapval  32151  hdmaplna2  32174  hdmapglnm2  32175  hdmapinvlem3  32184  hlhilset  32198  hlhilipval  32213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rex 2634  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366
  Copyright terms: Public domain W3C validator