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

Theorem fveq1d 5776
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 5773 . 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 1399   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504
This theorem is referenced by:  fveq12d  5780  funssfv  5789  csbfv12  5809  csbfv2g  5810  fvmptd  5862  fvmpt2d  5867  mpteqb  5872  fvmptt  5873  fnmptfvd  5892  fmptco  5966  fvunsn  6005  fvsng  6007  fsnunfv  6013  f1ocnvfv1  6083  f1ocnvfv2  6084  fcof1  6091  fcofo  6092  csbov123  6230  elovmpt3rab1  6435  ofval  6448  offval2  6455  ofrfval2  6456  caofinvl  6466  curry1val  6792  curry2val  6796  fnwelem  6814  fvmpt2curryd  6918  rdg0g  7011  oav  7079  omv  7080  oev  7082  resixpfo  7426  pw2f1olem  7540  mapxpen  7602  xpmapenlem  7603  ordtypelem6  7863  ordtypelem7  7864  unwdomg  7925  cantnffval  7993  cantnfval  8000  cantnfres  8009  cantnfp1lem3  8012  cantnfvalOLD  8030  cantnfp1lem3OLD  8038  fseqenlem1  8318  fseqenlem2  8319  iunfictbso  8408  dfac12lem1  8436  dfac12lem2  8437  dfac12r  8439  ackbij2lem3  8534  ituni0  8711  itunisuc  8712  itunitc1  8713  ituniiun  8715  hsmexlem2  8720  hsmexlem4  8722  iundom2g  8828  konigthlem  8856  konigth  8857  fpwwe2lem6  8924  fpwwe2lem9  8927  rpnnen1lem3  11129  rpnnen1lem5  11131  fseq1p1m1  11674  seqp1  12025  seqf1olem2  12050  seqf1o  12051  seqid  12055  seqz  12058  seqof  12067  seqof2  12068  bcval5  12298  bcn2  12299  hashf1lem1  12408  seqcoll  12416  s1fv  12528  ccat2s1fvw  12551  swrdfv  12560  swrdswrd  12596  splfv1  12642  revfv  12648  cshwidxmod  12685  ccat2s1fvwALT  12804  relexpsucnnr  12862  shftcan1  12918  shftcan2  12919  climshft2  13407  isercoll2  13493  sumeq2w  13516  sumeq2ii  13517  summo  13541  fsum  13544  fsumss  13549  fsumcvg2  13551  isumsplit  13654  prodeq2w  13721  prodeq2ii  13722  prodmo  13745  fprod  13750  fprodss  13757  rpnnen2lem1  13950  rpnnen2  13961  ruclem4  13969  sadfval  14104  smufval  14129  odzval  14320  1arithlem2  14444  vdwpc  14500  vdwlem6  14506  ramval  14528  fvsetsid  14661  setsid  14677  setsnid  14678  prdsval  14862  prdsplusgfval  14881  prdsmulrfval  14883  pwsvscaval  14902  imasval  14918  xpsc0  14967  xpsc1  14968  mrisval  15037  comfffval  15104  sectffval  15156  invinv  15176  oppcsect  15184  invisoinvl  15196  brcic  15204  brssc  15220  issubc  15241  isfunc  15270  funcoppc  15281  idfuval  15282  idfu2  15284  idfu1  15286  idfucl  15287  cofuval  15288  cofu1  15290  cofu2  15292  cofuval2  15293  cofucl  15294  cofurid  15297  resfval  15298  resfval2  15299  funcres  15302  funcpropd  15306  isfull  15316  isnat  15353  fucco  15368  homafval  15425  idafval  15453  setcmon  15483  catcisolem  15502  catciso  15503  funcestrcsetclem6  15531  funcsetcestrclem6  15546  xpcval  15563  1stf1  15578  2ndf1  15581  1stfcl  15583  2ndfcl  15584  prfval  15585  prf2fval  15587  prf1st  15590  prf2nd  15591  1st2ndprf  15592  evlf2  15604  evlf2val  15605  evlfcl  15608  curfval  15609  curfpropd  15619  uncfval  15620  uncf2  15623  curfuncf  15624  diag11  15629  diag12  15630  diag2  15631  curf2ndf  15633  hofval  15638  hofcl  15645  yon11  15650  yon12  15651  yon2  15652  yonedalem4a  15661  yonedalem4b  15662  yonedalem4c  15663  yonedalem22  15664  yonedalem3b  15665  yonedainv  15667  yoniso  15671  lubval  15731  glbval  15744  poslubdg  15896  gsumvalx  16014  gsumpropd  16016  gsumress  16020  gsumval2a  16023  prdspjmhm  16115  pwsco1mhm  16118  grpsubfval  16209  grplactval  16254  grpsubpropd  16257  grpsubpropd2  16258  mulgfval  16260  mulgpropd  16292  submmulg  16294  pwsinvg  16299  subgmulg  16332  eqgfval  16366  cntrval  16474  cntzval  16476  cntzrcl  16482  oppgsubg  16515  lactghmga  16546  symgga  16548  gsmsymgrfixlem1  16569  gsmsymgrfix  16570  gsmsymgreqlem1  16572  gsmsymgreqlem2  16573  gsmsymgreq  16574  pmtrval  16593  pmtrfv  16594  pmtrffv  16601  pmtrdifwrdellem3  16625  pmtrdifwrdel2lem1  16626  pmtrdifwrdel  16627  pmtrdifwrdel2  16628  ispgp  16729  vrgpval  16902  frgpup3lem  16912  frgpnabllem1  16994  frgpnabllem2  16995  gsumval3eu  17024  gsumval3OLD  17025  gsumval3lem2  17027  gsumval3  17028  gsumzres  17031  gsumzf1o  17034  gsumzresOLD  17035  gsumzf1oOLD  17037  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumconst  17070  dmdprd  17142  dprdval  17147  dprdvalOLD  17149  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  dprd2da  17204  dpjfval  17217  dpjidcl  17220  dpjlid  17223  dpjrid  17224  dpjidclOLD  17227  dvrfval  17446  staffval  17609  srngnvl  17618  issrngd  17623  lspval  17734  islbs  17835  lbspropd  17858  lssacsex  17903  lbsacsbs  17915  sralem  17936  srasca  17940  sravsca  17941  sraip  17942  rlmval  17950  ixpsnbasval  17968  lpival  18006  rrgsupp  18052  aspval  18090  psrmulval  18152  psrvscaval  18158  psrdi  18174  psrdir  18175  mvrval  18190  mvrval2  18191  mvrf1  18194  mplsubglem  18206  mplsubglemOLD  18208  mplvscaval  18223  subrgmvrf  18237  opsrle  18253  opsrbaslem  18255  subrgasclcl  18277  evlslem1  18297  evlsval  18301  evlssca  18304  evlsvar  18305  evlval  18306  evlsscasrng  18308  evlsvarsrng  18310  evlvar  18311  psr1val  18338  vr1val  18344  coe1fv  18358  subrgvr1  18415  coe1addfv  18419  coe1subfv  18420  coe1tmfv1  18428  coe1tmfv2  18429  coe1tmmul2fv  18432  coe1pwmulfv  18434  coe1sclmulfv  18437  ply1sclid  18442  ply1sclf1  18443  ply1coe1eq  18453  cply1coe0bi  18455  coe1fzgsumdlem  18456  coe1fzgsumd  18457  gsummoncoe1  18459  gsumply1eq  18460  evls1val  18470  evls1sca  18473  evl1sca  18483  evl1scad  18484  evl1var  18485  evl1vard  18486  evls1var  18487  evls1scasrng  18488  evls1varsrng  18489  evl1addd  18490  evl1subd  18491  evl1muld  18492  evl1vsd  18493  evl1expd  18494  pf1ind  18504  evl1gsumdlem  18505  evl1gsumd  18506  evl1gsumadd  18507  zrhmulg  18640  chrval  18655  chrrhm  18661  znzrhval  18676  psgndiflemA  18728  ocvval  18789  elocv  18790  cssval  18804  pjfval  18828  pjfo  18837  isobs  18842  dsmmval  18856  dsmm0cl  18862  prdsinvgd2  18864  frlmvscaval  18889  frlmphl  18901  uvcval  18905  uvcvval  18906  uvcresum  18913  mat1dimscm  19062  mat1rhmelval  19067  marepvval  19154  mdetfval  19173  mdetleib2  19175  mdet0fv0  19181  m1detdiag  19184  mdetdiaglem  19185  mdetralt  19195  mdetunilem7  19205  mdetuni0  19208  m2detleiblem1  19211  smadiadetr  19262  cramerimplem1  19270  cpmatel  19297  1elcpmat  19301  cpmatinvcl  19303  cpmatmcllem  19304  cpmatmcl  19305  mat2pmatfval  19309  m2cpm  19327  cpm2mval  19336  cpm2mvalel  19337  m2cpminvid  19339  m2cpminvid2lem  19340  m2cpminvid2  19341  m2cpmfo  19342  decpmate  19352  decpmatid  19356  decpmatmullem  19357  decpmatmulsumfsupp  19359  monmatcollpw  19365  pmatcollpw3lem  19369  pmatcollpwscmatlem1  19375  pmatcollpwscmatlem2  19376  pm2mpf1  19385  pm2mpcoe1  19386  mply1topmatval  19390  mp2pm2mplem1  19392  mp2pm2mplem3  19394  mp2pm2mplem4  19395  mp2pm2mp  19397  pm2mpghm  19402  pm2mpmhmlem1  19404  pm2mpmhmlem2  19405  chpmatfval  19416  chpmat0d  19420  chpscmatgsumbin  19430  cayleyhamilton0  19475  cayleyhamiltonALT  19477  ntrval  19622  clsval  19623  opncldf3  19673  neival  19689  neiptopreu  19720  lpfval  19725  lpval  19726  cnpval  19823  iscnp2  19826  isreg  19919  isnrm  19922  2ndcsep  20045  isnlly  20055  ptval  20156  dfac14  20204  cnmptk2  20272  pt1hmeo  20392  xkocnv  20400  fmval  20529  ufldom  20548  flimval  20549  flffval  20575  flfval  20576  cnpflf  20587  txflf  20592  fclsval  20594  fcfval  20619  cnextval  20646  cnextfvval  20650  cnextcn  20652  cnextfres  20653  symgtgp  20685  tgpconcomp  20696  prdstmdd  20707  utopsnneiplem  20835  neipcfilu  20884  txmetcnp  21135  subgnm2  21233  tngngp  21253  isnlm  21269  sranlm  21278  lssnlm  21294  nmofval  21306  nmoval  21307  isphtpy  21566  pcovalg  21597  pco1  21600  clmneg  21666  clmabs  21667  nmoleub2lem3  21683  nmoleub3  21687  cphcjcl  21715  cphnm  21725  cphipcj  21731  cphassr  21743  tchnmval  21757  tchcphlem3  21761  ipcau2  21762  tchcphlem1  21763  tchcphlem2  21764  tchcph  21765  ipcau  21766  rrxnm  21908  rrxmval  21917  ovolctb  21986  voliunlem3  22047  uniioombllem2  22077  vitalilem4  22105  mbflimsup  22158  itg1climres  22206  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  mbfi1fseqlem6  22212  mbfi1flimlem  22214  mbfmullem2  22216  mbfmullem  22217  itg2monolem1  22242  itg2mono  22245  itg2i1fseqle  22246  itg2i1fseq  22247  itg2addlem  22250  itg2cnlem1  22253  limcfval  22361  limcmpt2  22373  limcres  22375  cnplimc  22376  dvfval  22386  dvreslem  22398  dvres2lem  22399  dvn0  22412  dvnp1  22413  cpnfval  22420  elcpn  22422  dvaddbr  22426  dvmulbr  22427  dvcmul  22432  dvfre  22439  rolle  22476  cmvth  22477  mvth  22478  dvlip  22479  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  dveq0  22486  dv11cn  22487  dvivthlem1  22494  dvivth  22496  dvne0  22497  lhop1lem  22499  lhop2  22501  lhop  22502  dvcnvrelem2  22504  dvcvx  22506  dvfsumabs  22509  ftc1lem6  22527  ftc2  22530  ftc2ditglem  22531  itgparts  22533  itgsubstlem  22534  mdegaddle  22559  mdegmullem  22563  coe1mul3  22585  uc1pval  22625  mon1pval  22627  uc1pmon1p  22637  q1pval  22639  ply1remlem  22648  ply1rem  22649  fta1glem2  22652  fta1g  22653  fta1blem  22654  ig1pval  22658  plyeq0lem  22692  coeeulem  22706  coeid2  22721  dgrle  22725  dgreq  22726  0dgrb  22728  dgrnznn  22729  coemul  22734  coe11  22735  coe1term  22741  dgrlt  22748  dgradd2  22750  dgrcolem2  22756  plymul0or  22762  plydivlem4  22777  plydiveu  22779  plyremlem  22785  plyrem  22786  fta1  22789  vieta1lem2  22792  plyexmo  22794  aareccl  22807  aannenlem1  22809  aannenlem2  22810  taylfval  22839  tayl0  22842  dvtaylp  22850  dvntaylp0  22852  taylthlem1  22853  taylthlem2  22854  ulmval  22860  ulmres  22868  ulmshftlem  22869  ulmshft  22870  ulmuni  22872  ulmcaulem  22874  ulmcau  22875  ulmss  22877  ulmdvlem1  22880  ulmdvlem3  22882  mtest  22884  mtestbdd  22885  mbfulm  22886  itgulm  22888  itgulm2  22889  pserval2  22891  pserulm  22902  psercn  22906  pserdvlem2  22908  pserdv  22909  pige3  22995  logtayl  23128  rlimcnp  23412  sqff1o  23573  muinv  23586  dchrinv  23653  sumdchr2  23662  dchr2sum  23665  lgsval4  23708  lgsmod  23713  lgsqrlem1  23733  dchrmusumlema  23795  dchrvmasumlem1  23797  dchrisum0re  23815  dchrisum0lema  23816  logsqvma2  23845  padicval  23919  istrkg2ld  23975  iscgrg  24024  midexlem  24189  israg  24194  colperpexlem2  24225  colperpexlem3  24226  opphllem  24229  midex  24231  mideu  24232  opphllem3  24241  midf  24262  ismidb  24264  lmieu  24270  lmimid  24279  brcgr  24324  ecgrtg  24407  wwlkn  24803  wlkiswwlkfun  24838  wlkiswwlkinj  24839  wlkiswwlksur  24840  wlkiswwlkbij2  24842  clwwlkn  24888  vdgrfval  25016  vdgrval  25017  isrgra  25047  isrgrac  25055  rusgranumwlklem4  25073  iseupa  25086  eupath2lem3  25100  eupath2  25101  vdfrgra0  25143  grpoinvval  25344  grpodivfval  25361  gxfval  25376  gxval  25377  imsdval  25709  sspnval  25767  nmoofval  25794  nmooval  25795  bloval  25813  0oval  25820  nmlno0  25827  hmoval  25842  ajval  25894  ubth  25906  htthlem  25951  pjhval  26432  pjoc1  26469  pjoc2  26474  pjige0  26726  pjcjt2  26727  pjch  26729  pjsumi  26745  pjdsi  26747  pjds3i  26748  pjopyth  26755  pjnorm  26759  pjpyth  26760  pjnel  26761  hosval  26775  homval  26776  hodval  26777  hfsval  26778  hfmval  26779  braval  26979  kbval  26989  eigvalval  26995  leopg  27157  leoppos  27161  leoprf2  27162  leoprf  27163  elpjrn  27225  pj3cor1i  27244  strlem2  27286  hstrlem2  27294  fmptcof2  27643  offval2f  27652  resf1o  27703  fpwrelmap  27706  fmcncfil  28067  nmmulg  28102  zrhnm  28103  qqhval  28108  qqhcn  28125  xrhval  28149  ofcfval  28246  ofcfval3  28250  brfae  28376  omsval  28420  sitgval  28457  eulerpartlemsv1  28478  eulerpartlemsf  28481  eulerpartlemgvv  28498  eulerpartlemn  28503  sseqval  28510  sseqfv1  28511  sseqfv2  28516  fibp1  28523  dstrvval  28592  ballotleme  28618  ballotlemi  28622  plymulx0  28687  plymulx  28688  signstfv  28703  signstfvneq0  28712  signstfvc  28714  signstres  28715  signstfveq0  28717  signsvvfval  28718  lgamgulmlem2  28761  lgamgulmlem5  28764  lgamgulm2  28767  lgamcvglem  28771  subfacp1lem5  28817  kur14  28849  ptpcon  28867  cvmliftmolem1  28915  cvmliftlem5  28923  cvmliftlem7  28925  cvmliftlem15  28932  cvmlift2lem3  28939  cvmlift2lem4  28940  cvmlift2lem7  28943  cvmlift2lem9  28945  cvmlift2  28950  cvmliftphtlem  28951  cvmlift3lem2  28954  cvmlift3lem5  28957  cvmlift3lem6  28958  cvmlift3lem7  28959  cvmlift3lem9  28961  cvmlift3  28962  mrsubfval  29057  msubffval  29072  msubfval  29073  mvhfval  29082  msubff1  29105  mclsval  29112  shftvalg  29281  bpolylem  29963  ftc2nc  30265  neibastop3  30346  tailval  30357  filnetlem4  30365  cocanfo  30374  f1ocan2fv  30384  upixp  30386  sdclem2  30401  rrncmslem  30494  ismrer1  30500  isnacs  30802  mzpsubst  30846  eldioph2  30860  pw2f1ocnv  31145  fnwe2lem2  31163  islnr3  31232  hbtlem1  31240  hbtlem2  31241  hbtlem7  31242  hbtlem4  31243  hbtlem5  31245  hbt  31247  dgrsub2  31252  mpaaeu  31267  mpaalem  31269  rgspnval  31285  flcidc  31291  cntzsdrg  31319  itgpowd  31350  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  addrfv  31546  subrfv  31547  mulvfv  31548  refsum2cnlem1  31579  n0p  31604  fvmpt2bd  31613  fmuldfeqlem1  31742  fmuldfeq  31743  fmul01lt1lem1  31744  fmul01lt1lem2  31745  limciccioolb  31793  limcicciooub  31809  cncfuni  31855  cncfiooicclem1  31862  dvsinax  31874  dvbdfbdioolem1  31891  dvnmptdivc  31901  dvnmul  31906  dvnprodlem1  31909  dvnprodlem2  31910  dvnprodlem3  31911  dvnprod  31912  itgsincmulx  31939  stoweidlem17  31965  stoweidlem20  31968  stoweidlem27  31975  stoweidlem31  31979  stoweidlem34  31982  stoweidlem44  31992  stoweidlem48  31996  stoweidlem59  32007  stirlinglem3  32024  stirlinglem15  32036  dirkeritg  32050  dirkercncflem2  32052  dirkercncflem3  32053  dirkercncflem4  32054  dirkercncf  32055  fourierdlem42  32097  fourierdlem60  32115  fourierdlem61  32116  fourierdlem68  32123  fourierdlem73  32128  fourierdlem80  32135  fourierdlem93  32148  fourierdlem94  32149  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  fourierdlem113  32168  elaa2lem  32182  elaa2  32183  etransclem17  32200  etransclem29  32212  etransclem32  32215  etransclem46  32229  pfxfv  32574  rngcid  32987  ringcid  33033  funcringcsetcALTV2lem6  33049  funcringcsetclem6ALTV  33072  coe1sclmulval  33185  ply1mulgsum  33190  evl1at0  33191  evl1at1  33192  lincvalpr  33219  aacllem  33550  bnj1379  34236  bj-finsumval0  35010  lshpset  35116  lsatset  35128  lkrval  35226  eqlkr  35237  ldualvaddval  35269  ldualvsval  35276  ldualvsubval  35295  cmtfvalN  35348  isoml  35376  pmapval  35894  pclvalN  36027  polfvalN  36041  polvalN  36042  psubclsetN  36073  watfvalN  36129  watvalN  36130  ldilset  36246  ltrnfset  36254  ltrnset  36255  dilfsetN  36290  dilsetN  36291  trnfsetN  36293  trnsetN  36294  trlfset  36298  trlset  36299  trlval  36300  ltrnideq  36313  cdlemd8  36343  cdlemg1idlemN  36711  cdlemg1fvawlemN  36712  cdlemg2idN  36735  trlcoabs2N  36861  tgrpfset  36883  tgrpset  36884  tendofset  36897  tendoset  36898  erngfset  36938  erngset  36939  erngfset-rN  36946  erngset-rN  36947  cdlemi2  36958  cdlemj1  36960  cdlemk2  36971  cdlemk4  36973  cdlemk8  36977  cdlemkuu  37034  cdlemk31  37035  cdlemkuv2-3N  37038  cdlemk18-3N  37039  cdlemk22-3  37040  cdlemkfid2N  37062  cdlemkyu  37066  cdlemk19ylem  37069  cdlemk46  37087  cdlemk49  37090  cdlemk43N  37102  cdlemk19u1  37108  cdlemk19u  37109  dvafset  37143  dvaset  37144  dvaplusgv  37149  diaffval  37170  diafval  37171  diaval  37172  dvhfset  37220  dvhset  37221  dvhlveclem  37248  docaffvalN  37261  docafvalN  37262  docavalN  37263  djaffvalN  37273  djafvalN  37274  dibffval  37280  dibfval  37281  dibval  37282  dicffval  37314  dicfval  37315  dicval  37316  dicelvalN  37318  dicvaddcl  37330  dicvscacl  37331  cdlemn8  37344  cdlemn9  37345  dihordlem7b  37355  dihffval  37370  dihfval  37371  dihval  37372  dihopelvalcpre  37388  dihmeetlem1N  37430  dihglblem5apreN  37431  dihmeetlem4preN  37446  dihmeetlem13N  37459  dih1dimatlem0  37468  dochffval  37489  dochfval  37490  dochval  37491  djhffval  37536  djhfval  37537  lcfl7lem  37639  lclkrlem2k  37657  lclkrlem2u  37667  lcdfval  37728  lcdval  37729  lcdvaddval  37738  lcdvsval  37744  lcd0vvalN  37753  lcdvsubval  37758  lcdlsp  37761  mapdffval  37766  mapdfval  37767  mapdval  37768  hvmapffval  37898  hvmapfval  37899  hvmapval  37900  hvmapvalvalN  37901  hvmapidN  37902  hvmaplkr  37908  hdmap1ffval  37936  hdmap1fval  37937  hdmap1vallem  37938  hdmapffval  37969  hdmapfval  37970  hdmapval  37971  hdmapevec2  37979  hgmapffval  38028  hgmapfval  38029  hgmapval  38030  hdmaplna2  38053  hdmapglnm2  38054  hdmapinvlem3  38063  hlhilset  38077  hlhilipval  38092
  Copyright terms: Public domain W3C validator