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

Theorem fveq1d 5681
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 5678 . 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 1362   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414
This theorem is referenced by:  fveq12d  5685  funssfv  5693  csbfv12  5713  csbfv2g  5715  fvmptd  5767  fvmpt2d  5771  mpteqb  5776  fvmptt  5777  fnmptfvd  5794  fmptco  5863  fvunsn  5897  fvsng  5899  fsnunfv  5905  f1ocnvfv1  5970  f1ocnvfv2  5971  fcof1  5978  fcofo  5979  csbov123  6111  ofval  6318  offval2  6325  ofrfval2  6326  caofinvl  6336  curry1val  6654  curry2val  6658  fnwelem  6676  rdg0g  6869  oav  6939  omv  6940  oev  6942  resixpfo  7289  pw2f1olem  7403  mapxpen  7465  xpmapenlem  7466  ordtypelem6  7725  ordtypelem7  7726  unwdomg  7787  cantnffval  7857  cantnfval  7864  cantnfres  7873  cantnfp1lem3  7876  cantnfvalOLD  7894  cantnfp1lem3OLD  7902  fseqenlem1  8182  fseqenlem2  8183  iunfictbso  8272  dfac12lem1  8300  dfac12lem2  8301  dfac12r  8303  ackbij2lem3  8398  ituni0  8575  itunisuc  8576  itunitc1  8577  ituniiun  8579  hsmexlem2  8584  hsmexlem4  8586  iundom2g  8692  konigthlem  8720  konigth  8721  fpwwe2lem6  8790  fpwwe2lem9  8793  rpnnen1lem3  10969  rpnnen1lem5  10971  fseq1p1m1  11518  seqp1  11805  seqf1olem2  11830  seqf1o  11831  seqid  11835  seqz  11838  seqof  11847  seqof2  11848  bcval5  12078  bcn2  12079  hashf1lem1  12192  seqcoll  12200  s1fv  12282  swrdfv  12304  swrdswrd  12338  splfv1  12381  revfv  12387  cshwidxmod  12424  shftcan1  12556  shftcan2  12557  climshft2  13044  isercoll2  13130  sumeq2w  13153  sumeq2ii  13154  summo  13178  fsum  13181  fsumss  13186  fsumcvg2  13188  isumsplit  13286  rpnnen2lem1  13480  rpnnen2  13491  ruclem4  13499  sadfval  13631  smufval  13656  odzval  13846  1arithlem2  13968  vdwpc  14024  vdwlem6  14030  ramval  14052  fvsetsid  14182  setsid  14198  setsnid  14199  prdsval  14376  prdsplusgfval  14395  prdsmulrfval  14397  pwsvscaval  14416  imasval  14432  xpsc0  14481  xpsc1  14482  mrisval  14551  comfffval  14620  sectffval  14672  invinv  14691  oppcsect  14695  brssc  14710  issubc  14731  isfunc  14757  funcoppc  14768  idfuval  14769  idfu2  14771  idfu1  14773  idfucl  14774  cofuval  14775  cofu1  14777  cofu2  14779  cofuval2  14780  cofucl  14781  cofurid  14784  resfval  14785  resfval2  14786  funcres  14789  funcpropd  14793  isfull  14803  isnat  14840  fucco  14855  homafval  14880  idafval  14908  setcmon  14938  catcisolem  14957  catciso  14958  xpcval  14970  1stf1  14985  2ndf1  14988  1stfcl  14990  2ndfcl  14991  prfval  14992  prf2fval  14994  prf1st  14997  prf2nd  14998  1st2ndprf  14999  evlf2  15011  evlf2val  15012  evlfcl  15015  curfval  15016  curfpropd  15026  uncfval  15027  uncf2  15030  curfuncf  15031  diag11  15036  diag12  15037  diag2  15038  curf2ndf  15040  hofval  15045  hofcl  15052  yon11  15057  yon12  15058  yon2  15059  yonedalem4a  15068  yonedalem4b  15069  yonedalem4c  15070  yonedalem22  15071  yonedalem3b  15072  yonedainv  15074  yoniso  15078  lubval  15137  glbval  15150  poslubdg  15302  prdspjmhm  15477  pwsco1mhm  15480  gsumvalx  15484  gsumpropd  15486  gsumress  15487  gsumval2a  15492  grpsubfval  15560  grplactval  15603  grpsubpropd  15606  grpsubpropd2  15607  mulgfval  15608  mulgpropd  15640  submmulg  15642  pwsinvg  15647  subgmulg  15675  eqgfval  15709  cntrval  15817  cntzval  15819  cntzrcl  15825  oppgsubg  15858  lactghmga  15889  symgga  15891  gsmsymgrfixlem1  15912  gsmsymgrfix  15913  gsmsymgreqlem1  15915  gsmsymgreqlem2  15916  gsmsymgreq  15917  pmtrval  15937  pmtrfv  15938  pmtrffv  15945  pmtrdifwrdellem3  15969  pmtrdifwrdel2lem1  15970  pmtrdifwrdel  15971  pmtrdifwrdel2  15972  ispgp  16071  vrgpval  16244  frgpup3lem  16254  frgpnabllem1  16331  frgpnabllem2  16332  gsumval3eu  16361  gsumval3OLD  16362  gsumval3lem2  16364  gsumval3  16365  gsumzres  16368  gsumzf1o  16371  gsumzresOLD  16372  gsumzf1oOLD  16374  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  dmdprd  16454  dprdval  16459  dprdvalOLD  16461  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  dprd2da  16515  dpjfval  16528  dpjidcl  16531  dpjlid  16534  dpjrid  16535  dpjidclOLD  16538  dvrfval  16710  staffval  16856  srngnvl  16865  issrngd  16870  lspval  16978  islbs  17079  lbspropd  17102  lssacsex  17147  lbsacsbs  17159  sralem  17180  srasca  17184  sravsca  17185  sraip  17186  rlmval  17194  ixpsnbasval  17212  lpival  17249  rrgsupp  17284  aspval  17321  psrmulval  17391  psrvscaval  17397  psrdi  17413  psrdir  17414  mvrval  17428  mvrval2  17429  mvrf1  17432  mplsubglem  17444  mplsubglemOLD  17446  mplvscaval  17461  subrgmvrf  17475  opsrle  17489  opsrbaslem  17491  subrgasclcl  17513  psr1val  17541  vr1val  17547  coe1fv  17561  subrgvr1  17613  coe1addfv  17617  coe1subfv  17618  coe1tmfv1  17625  coe1tmfv2  17626  coe1tmmul2fv  17629  coe1pwmulfv  17631  coe1sclmulfv  17634  ply1sclid  17638  ply1sclf1  17639  zrhmulg  17783  chrval  17798  chrrhm  17804  znzrhval  17821  psgndiflemA  17873  ocvval  17934  elocv  17935  cssval  17949  pjfval  17973  pjfo  17982  isobs  17987  dsmmval  18001  dsmm0cl  18007  prdsinvgd2  18009  frlmvscaval  18036  frlmphl  18048  uvcval  18052  uvcvval  18053  uvcresum  18060  marepvval  18220  mdetfval  18239  mdetleib2  18241  mdet0fv0  18247  mdetralt  18256  mdetunilem7  18266  mdetuni0  18269  m2detleiblem1  18272  smadiadetr  18323  cramerimplem1  18331  ntrval  18482  clsval  18483  opncldf3  18532  neival  18548  neiptopreu  18579  lpfval  18584  lpval  18585  cnpval  18682  iscnp2  18685  isreg  18778  isnrm  18781  2ndcsep  18905  isnlly  18915  ptval  18985  dfac14  19033  cnmptk2  19101  pt1hmeo  19221  xkocnv  19229  fmval  19358  ufldom  19377  flimval  19378  flffval  19404  flfval  19405  cnpflf  19416  txflf  19421  fclsval  19423  fcfval  19448  cnextval  19475  cnextfvval  19479  cnextcn  19481  cnextfres  19482  symgtgp  19514  tgpconcomp  19525  prdstmdd  19536  utopsnneiplem  19664  neipcfilu  19713  txmetcnp  19964  subgnm2  20062  tngngp  20082  isnlm  20098  sranlm  20107  lssnlm  20123  nmofval  20135  nmoval  20136  isphtpy  20395  pcovalg  20426  pco1  20429  clmneg  20495  clmabs  20496  nmoleub2lem3  20512  nmoleub3  20516  cphcjcl  20544  cphnm  20554  cphipcj  20560  cphassr  20572  tchnmval  20586  tchcphlem3  20590  ipcau2  20591  tchcphlem1  20592  tchcphlem2  20593  tchcph  20594  ipcau  20595  rrxnm  20737  ovolctb  20815  voliunlem3  20875  uniioombllem2  20905  vitalilem4  20933  mbflimsup  20986  itg1climres  21034  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1fseqlem6  21040  mbfi1flimlem  21042  mbfmullem2  21044  mbfmullem  21045  itg2monolem1  21070  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq  21075  itg2addlem  21078  itg2cnlem1  21081  limcfval  21189  limcmpt2  21201  limcres  21203  cnplimc  21204  dvfval  21214  dvreslem  21226  dvres2lem  21227  dvn0  21240  dvnp1  21241  cpnfval  21248  elcpn  21250  dvaddbr  21254  dvmulbr  21255  dvcmul  21260  dvfre  21267  rolle  21304  cmvth  21305  mvth  21306  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  dveq0  21314  dv11cn  21315  dvivthlem1  21322  dvivth  21324  dvne0  21325  lhop1lem  21327  lhop2  21329  lhop  21330  dvcnvrelem2  21332  dvcvx  21334  dvfsumabs  21337  ftc1lem6  21355  ftc2  21358  ftc2ditglem  21359  itgparts  21361  itgsubstlem  21362  evlslem1  21367  evlsval  21371  evlssca  21374  evlsvar  21375  evlval  21376  evl1sca  21381  evl1scad  21382  evl1var  21383  evl1vard  21384  evl1addd  21385  evl1subd  21386  evl1muld  21387  evl1vsd  21388  evl1expd  21389  pf1ind  21406  mdegaddle  21430  mdegmullem  21434  coe1mul3  21456  uc1pval  21496  mon1pval  21498  uc1pmon1p  21508  q1pval  21510  ply1remlem  21519  ply1rem  21520  fta1glem2  21523  fta1g  21524  fta1blem  21525  ig1pval  21529  plyeq0lem  21563  coeeulem  21577  coeid2  21592  dgrle  21596  dgreq  21597  0dgrb  21599  coemul  21604  coe11  21605  coe1term  21611  dgrlt  21618  dgradd2  21620  dgrcolem2  21626  plymul0or  21632  plydivlem4  21647  plydiveu  21649  plyremlem  21655  plyrem  21656  fta1  21659  vieta1lem2  21662  plyexmo  21664  aareccl  21677  aannenlem1  21679  aannenlem2  21680  taylfval  21709  tayl0  21712  dvtaylp  21720  dvntaylp0  21722  taylthlem1  21723  taylthlem2  21724  ulmval  21730  ulmres  21738  ulmshftlem  21739  ulmshft  21740  ulmuni  21742  ulmcaulem  21744  ulmcau  21745  ulmss  21747  ulmdvlem1  21750  ulmdvlem3  21752  mtest  21754  mtestbdd  21755  mbfulm  21756  itgulm  21758  itgulm2  21759  pserval2  21761  pserulm  21772  psercn  21776  pserdvlem2  21778  pserdv  21779  pige3  21864  logtayl  21990  rlimcnp  22244  sqff1o  22405  muinv  22418  dchrinv  22485  sumdchr2  22494  dchr2sum  22497  lgsval4  22540  lgsmod  22545  lgsqrlem1  22565  dchrmusumlema  22627  dchrvmasumlem1  22629  dchrisum0re  22647  dchrisum0lema  22648  logsqvma2  22677  padicval  22751  iscgrg  22846  brcgr  22969  ecgrtg  23052  vdgrfval  23388  vdgrval  23389  iseupa  23409  eupath2lem3  23423  eupath2  23424  grpoinvval  23535  grpodivfval  23552  gxfval  23567  gxval  23568  imsdval  23900  sspnval  23958  nmoofval  23985  nmooval  23986  bloval  24004  0oval  24011  nmlno0  24018  hmoval  24033  ajval  24085  ubth  24097  htthlem  24142  pjhval  24623  pjoc1  24660  pjoc2  24665  pjige0  24917  pjcjt2  24918  pjch  24920  pjsumi  24936  pjdsi  24938  pjds3i  24939  pjopyth  24946  pjnorm  24950  pjpyth  24951  pjnel  24952  hosval  24967  homval  24968  hodval  24969  hfsval  24970  hfmval  24971  braval  25171  kbval  25181  eigvalval  25187  leopg  25349  leoppos  25353  leoprf2  25354  leoprf  25355  elpjrn  25417  pj3cor1i  25436  strlem2  25478  hstrlem2  25486  fmptcof2  25803  offval2f  25807  resf1o  25855  fpwrelmap  25858  fmcncfil  26215  nmmulg  26251  zrhnm  26252  qqhval  26257  qqhcn  26274  ofcfval  26394  ofcfval3  26398  brfae  26518  sitgval  26566  eulerpartlemsv1  26587  eulerpartlemsf  26590  eulerpartlemgvv  26607  eulerpartlemn  26612  sseqval  26619  sseqfv1  26620  sseqfv2  26625  fibp1  26632  dstrvval  26701  ballotleme  26727  ballotlemi  26731  plymulx0  26796  plymulx  26797  signstfv  26812  signstfvneq0  26821  signstfvc  26823  signstres  26824  signstfveq0  26826  lgamgulmlem2  26864  lgamgulmlem5  26867  lgamgulm2  26870  lgamcvglem  26874  subfacp1lem5  26920  kur14  26952  ptpcon  26970  cvmliftmolem1  27018  cvmliftlem5  27026  cvmliftlem7  27028  cvmliftlem15  27035  cvmlift2lem3  27042  cvmlift2lem4  27043  cvmlift2lem7  27046  cvmlift2lem9  27048  cvmlift2  27053  cvmliftphtlem  27054  cvmlift3lem2  27057  cvmlift3lem5  27060  cvmlift3lem6  27061  cvmlift3lem7  27062  cvmlift3lem9  27064  cvmlift3  27065  relexp0  27178  relexpsucr  27179  shftvalg  27242  prodeq2w  27272  prodeq2ii  27273  prodmo  27296  fprod  27301  fprodss  27308  bpolylem  28038  ftc2nc  28320  neibastop3  28427  tailval  28438  filnetlem4  28446  cocanfo  28455  f1ocan2fv  28465  upixp  28467  sdclem2  28482  rrncmslem  28575  ismrer1  28581  isnacs  28885  mzpsubst  28930  eldioph2  28945  pw2f1ocnv  29231  fnwe2lem2  29249  islnr3  29316  hbtlem1  29324  hbtlem2  29325  hbtlem7  29326  hbtlem4  29327  hbtlem5  29329  hbt  29331  dgrsub2  29336  dgrnznn  29337  mpaaeu  29352  mpaalem  29354  rgspnval  29370  flcidc  29376  cntzsdrg  29404  itgpowd  29435  addrfv  29570  subrfv  29571  mulvfv  29572  refsum2cnlem1  29604  fmuldfeqlem1  29608  fmuldfeq  29609  fmul01lt1lem1  29610  fmul01lt1lem2  29611  stoweidlem17  29658  stoweidlem20  29661  stoweidlem27  29668  stoweidlem31  29672  stoweidlem34  29675  stoweidlem42  29683  stoweidlem44  29685  stoweidlem48  29689  stoweidlem59  29700  stirlinglem3  29717  stirlinglem15  29729  elovmpt3rab1  30009  ccatw2s1p1  30115  ccatw2s1p2  30116  ccat2s1fvw  30117  wwlkn  30162  wlkiswwlkfun  30195  wlkiswwlkinj  30196  wlkiswwlksur  30197  wlkiswwlkbij2  30199  clwwlkn  30276  isrgra  30389  rusgranumwlklem4  30416  vdfrgra0  30460  vdgfrgra0  30461  evl1at0  30631  evl1at1  30632  lincvalpr  30661  bnj1379  31526  bj-finsumval0  32159  lshpset  32196  lsatset  32208  lkrval  32306  eqlkr  32317  ldualvaddval  32349  ldualvsval  32356  ldualvsubval  32375  cmtfvalN  32428  isoml  32456  pmapval  32974  pclvalN  33107  polfvalN  33121  polvalN  33122  psubclsetN  33153  watfvalN  33209  watvalN  33210  ldilset  33326  ltrnfset  33334  ltrnset  33335  dilfsetN  33369  dilsetN  33370  trnfsetN  33372  trnsetN  33373  trlfset  33377  trlset  33378  trlval  33379  ltrnideq  33392  cdlemd8  33422  cdlemg1idlemN  33789  cdlemg1fvawlemN  33790  cdlemg2idN  33813  trlcoabs2N  33939  tgrpfset  33961  tgrpset  33962  tendofset  33975  tendoset  33976  erngfset  34016  erngset  34017  erngfset-rN  34024  erngset-rN  34025  cdlemi2  34036  cdlemj1  34038  cdlemk2  34049  cdlemk4  34051  cdlemk8  34055  cdlemkuu  34112  cdlemk31  34113  cdlemkuv2-3N  34116  cdlemk18-3N  34117  cdlemk22-3  34118  cdlemkfid2N  34140  cdlemkyu  34144  cdlemk19ylem  34147  cdlemk46  34165  cdlemk49  34168  cdlemk43N  34180  cdlemk19u1  34186  cdlemk19u  34187  dvafset  34221  dvaset  34222  dvaplusgv  34227  diaffval  34248  diafval  34249  diaval  34250  dvhfset  34298  dvhset  34299  dvhlveclem  34326  docaffvalN  34339  docafvalN  34340  docavalN  34341  djaffvalN  34351  djafvalN  34352  dibffval  34358  dibfval  34359  dibval  34360  dicffval  34392  dicfval  34393  dicval  34394  dicelvalN  34396  dicvaddcl  34408  dicvscacl  34409  cdlemn8  34422  cdlemn9  34423  dihordlem7b  34433  dihffval  34448  dihfval  34449  dihval  34450  dihopelvalcpre  34466  dihmeetlem1N  34508  dihglblem5apreN  34509  dihmeetlem4preN  34524  dihmeetlem13N  34537  dih1dimatlem0  34546  dochffval  34567  dochfval  34568  dochval  34569  djhffval  34614  djhfval  34615  lcfl7lem  34717  lclkrlem2k  34735  lclkrlem2u  34745  lcdfval  34806  lcdval  34807  lcdvaddval  34816  lcdvsval  34822  lcd0vvalN  34831  lcdvsubval  34836  lcdlsp  34839  mapdffval  34844  mapdfval  34845  mapdval  34846  hvmapffval  34976  hvmapfval  34977  hvmapval  34978  hvmapvalvalN  34979  hvmapidN  34980  hvmaplkr  34986  hdmap1ffval  35014  hdmap1fval  35015  hdmap1vallem  35016  hdmapffval  35047  hdmapfval  35048  hdmapval  35049  hdmapevec2  35057  hgmapffval  35106  hgmapfval  35107  hgmapval  35108  hdmaplna2  35131  hdmapglnm2  35132  hdmapinvlem3  35141  hlhilset  35155  hlhilipval  35170
  Copyright terms: Public domain W3C validator