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

Theorem fveq1d 5688
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 5685 . 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 1369   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421
This theorem is referenced by:  fveq12d  5692  funssfv  5700  csbfv12  5720  csbfv2g  5722  fvmptd  5774  fvmpt2d  5778  mpteqb  5783  fvmptt  5784  fnmptfvd  5801  fmptco  5871  fvunsn  5905  fvsng  5907  fsnunfv  5913  f1ocnvfv1  5978  f1ocnvfv2  5979  fcof1  5986  fcofo  5987  csbov123  6117  ofval  6324  offval2  6331  ofrfval2  6332  caofinvl  6342  curry1val  6660  curry2val  6664  fnwelem  6682  rdg0g  6875  oav  6943  omv  6944  oev  6946  resixpfo  7293  pw2f1olem  7407  mapxpen  7469  xpmapenlem  7470  ordtypelem6  7729  ordtypelem7  7730  unwdomg  7791  cantnffval  7861  cantnfval  7868  cantnfres  7877  cantnfp1lem3  7880  cantnfvalOLD  7898  cantnfp1lem3OLD  7906  fseqenlem1  8186  fseqenlem2  8187  iunfictbso  8276  dfac12lem1  8304  dfac12lem2  8305  dfac12r  8307  ackbij2lem3  8402  ituni0  8579  itunisuc  8580  itunitc1  8581  ituniiun  8583  hsmexlem2  8588  hsmexlem4  8590  iundom2g  8696  konigthlem  8724  konigth  8725  fpwwe2lem6  8794  fpwwe2lem9  8797  rpnnen1lem3  10973  rpnnen1lem5  10975  fseq1p1m1  11526  seqp1  11813  seqf1olem2  11838  seqf1o  11839  seqid  11843  seqz  11846  seqof  11855  seqof2  11856  bcval5  12086  bcn2  12087  hashf1lem1  12200  seqcoll  12208  s1fv  12290  swrdfv  12312  swrdswrd  12346  splfv1  12389  revfv  12395  cshwidxmod  12432  shftcan1  12564  shftcan2  12565  climshft2  13052  isercoll2  13138  sumeq2w  13161  sumeq2ii  13162  summo  13186  fsum  13189  fsumss  13194  fsumcvg2  13196  isumsplit  13295  rpnnen2lem1  13489  rpnnen2  13500  ruclem4  13508  sadfval  13640  smufval  13665  odzval  13855  1arithlem2  13977  vdwpc  14033  vdwlem6  14039  ramval  14061  fvsetsid  14191  setsid  14207  setsnid  14208  prdsval  14385  prdsplusgfval  14404  prdsmulrfval  14406  pwsvscaval  14425  imasval  14441  xpsc0  14490  xpsc1  14491  mrisval  14560  comfffval  14629  sectffval  14681  invinv  14700  oppcsect  14704  brssc  14719  issubc  14740  isfunc  14766  funcoppc  14777  idfuval  14778  idfu2  14780  idfu1  14782  idfucl  14783  cofuval  14784  cofu1  14786  cofu2  14788  cofuval2  14789  cofucl  14790  cofurid  14793  resfval  14794  resfval2  14795  funcres  14798  funcpropd  14802  isfull  14812  isnat  14849  fucco  14864  homafval  14889  idafval  14917  setcmon  14947  catcisolem  14966  catciso  14967  xpcval  14979  1stf1  14994  2ndf1  14997  1stfcl  14999  2ndfcl  15000  prfval  15001  prf2fval  15003  prf1st  15006  prf2nd  15007  1st2ndprf  15008  evlf2  15020  evlf2val  15021  evlfcl  15024  curfval  15025  curfpropd  15035  uncfval  15036  uncf2  15039  curfuncf  15040  diag11  15045  diag12  15046  diag2  15047  curf2ndf  15049  hofval  15054  hofcl  15061  yon11  15066  yon12  15067  yon2  15068  yonedalem4a  15077  yonedalem4b  15078  yonedalem4c  15079  yonedalem22  15080  yonedalem3b  15081  yonedainv  15083  yoniso  15087  lubval  15146  glbval  15159  poslubdg  15311  prdspjmhm  15486  pwsco1mhm  15489  gsumvalx  15493  gsumpropd  15495  gsumress  15498  gsumval2a  15503  grpsubfval  15571  grplactval  15614  grpsubpropd  15617  grpsubpropd2  15618  mulgfval  15619  mulgpropd  15651  submmulg  15653  pwsinvg  15658  subgmulg  15686  eqgfval  15720  cntrval  15828  cntzval  15830  cntzrcl  15836  oppgsubg  15869  lactghmga  15900  symgga  15902  gsmsymgrfixlem1  15923  gsmsymgrfix  15924  gsmsymgreqlem1  15926  gsmsymgreqlem2  15927  gsmsymgreq  15928  pmtrval  15948  pmtrfv  15949  pmtrffv  15956  pmtrdifwrdellem3  15980  pmtrdifwrdel2lem1  15981  pmtrdifwrdel  15982  pmtrdifwrdel2  15983  ispgp  16082  vrgpval  16255  frgpup3lem  16265  frgpnabllem1  16342  frgpnabllem2  16343  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem2  16375  gsumval3  16376  gsumzres  16379  gsumzf1o  16382  gsumzresOLD  16383  gsumzf1oOLD  16385  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  dmdprd  16468  dprdval  16473  dprdvalOLD  16475  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  dprd2da  16529  dpjfval  16542  dpjidcl  16545  dpjlid  16548  dpjrid  16549  dpjidclOLD  16552  dvrfval  16764  staffval  16910  srngnvl  16919  issrngd  16924  lspval  17033  islbs  17134  lbspropd  17157  lssacsex  17202  lbsacsbs  17214  sralem  17235  srasca  17239  sravsca  17240  sraip  17241  rlmval  17249  ixpsnbasval  17267  lpival  17304  rrgsupp  17339  aspval  17376  psrmulval  17434  psrvscaval  17440  psrdi  17456  psrdir  17457  mvrval  17471  mvrval2  17472  mvrf1  17475  mplsubglem  17487  mplsubglemOLD  17489  mplvscaval  17504  subrgmvrf  17518  opsrle  17532  opsrbaslem  17534  subrgasclcl  17556  evlslem1  17576  evlsval  17580  evlssca  17583  evlsvar  17584  evlval  17585  evlsscasrng  17587  evlsvarsrng  17589  evlvar  17590  psr1val  17617  vr1val  17623  coe1fv  17637  subrgvr1  17690  coe1addfv  17694  coe1subfv  17695  coe1tmfv1  17702  coe1tmfv2  17703  coe1tmmul2fv  17706  coe1pwmulfv  17708  coe1sclmulfv  17711  ply1sclid  17715  ply1sclf1  17716  evls1val  17730  evls1sca  17733  evl1sca  17743  evl1scad  17744  evl1var  17745  evl1vard  17746  evls1var  17747  evls1scasrng  17748  evls1varsrng  17749  evl1addd  17750  evl1subd  17751  evl1muld  17752  evl1vsd  17753  evl1expd  17754  pf1ind  17764  evl1gsumdlem  17765  evl1gsumd  17766  evl1gsumadd  17767  zrhmulg  17916  chrval  17931  chrrhm  17937  znzrhval  17954  psgndiflemA  18006  ocvval  18067  elocv  18068  cssval  18082  pjfval  18106  pjfo  18115  isobs  18120  dsmmval  18134  dsmm0cl  18140  prdsinvgd2  18142  frlmvscaval  18169  frlmphl  18181  uvcval  18185  uvcvval  18186  uvcresum  18193  marepvval  18353  mdetfval  18372  mdetleib2  18374  mdet0fv0  18380  mdetralt  18389  mdetunilem7  18399  mdetuni0  18402  m2detleiblem1  18405  smadiadetr  18456  cramerimplem1  18464  ntrval  18615  clsval  18616  opncldf3  18665  neival  18681  neiptopreu  18712  lpfval  18717  lpval  18718  cnpval  18815  iscnp2  18818  isreg  18911  isnrm  18914  2ndcsep  19038  isnlly  19048  ptval  19118  dfac14  19166  cnmptk2  19234  pt1hmeo  19354  xkocnv  19362  fmval  19491  ufldom  19510  flimval  19511  flffval  19537  flfval  19538  cnpflf  19549  txflf  19554  fclsval  19556  fcfval  19581  cnextval  19608  cnextfvval  19612  cnextcn  19614  cnextfres  19615  symgtgp  19647  tgpconcomp  19658  prdstmdd  19669  utopsnneiplem  19797  neipcfilu  19846  txmetcnp  20097  subgnm2  20195  tngngp  20215  isnlm  20231  sranlm  20240  lssnlm  20256  nmofval  20268  nmoval  20269  isphtpy  20528  pcovalg  20559  pco1  20562  clmneg  20628  clmabs  20629  nmoleub2lem3  20645  nmoleub3  20649  cphcjcl  20677  cphnm  20687  cphipcj  20693  cphassr  20705  tchnmval  20719  tchcphlem3  20723  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  tchcph  20727  ipcau  20728  rrxnm  20870  ovolctb  20948  voliunlem3  21008  uniioombllem2  21038  vitalilem4  21066  mbflimsup  21119  itg1climres  21167  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  mbfi1flimlem  21175  mbfmullem2  21177  mbfmullem  21178  itg2monolem1  21203  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq  21208  itg2addlem  21211  itg2cnlem1  21214  limcfval  21322  limcmpt2  21334  limcres  21336  cnplimc  21337  dvfval  21347  dvreslem  21359  dvres2lem  21360  dvn0  21373  dvnp1  21374  cpnfval  21381  elcpn  21383  dvaddbr  21387  dvmulbr  21388  dvcmul  21393  dvfre  21400  rolle  21437  cmvth  21438  mvth  21439  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  dveq0  21447  dv11cn  21448  dvivthlem1  21455  dvivth  21457  dvne0  21458  lhop1lem  21460  lhop2  21462  lhop  21463  dvcnvrelem2  21465  dvcvx  21467  dvfsumabs  21470  ftc1lem6  21488  ftc2  21491  ftc2ditglem  21492  itgparts  21494  itgsubstlem  21495  mdegaddle  21520  mdegmullem  21524  coe1mul3  21546  uc1pval  21586  mon1pval  21588  uc1pmon1p  21598  q1pval  21600  ply1remlem  21609  ply1rem  21610  fta1glem2  21613  fta1g  21614  fta1blem  21615  ig1pval  21619  plyeq0lem  21653  coeeulem  21667  coeid2  21682  dgrle  21686  dgreq  21687  0dgrb  21689  coemul  21694  coe11  21695  coe1term  21701  dgrlt  21708  dgradd2  21710  dgrcolem2  21716  plymul0or  21722  plydivlem4  21737  plydiveu  21739  plyremlem  21745  plyrem  21746  fta1  21749  vieta1lem2  21752  plyexmo  21754  aareccl  21767  aannenlem1  21769  aannenlem2  21770  taylfval  21799  tayl0  21802  dvtaylp  21810  dvntaylp0  21812  taylthlem1  21813  taylthlem2  21814  ulmval  21820  ulmres  21828  ulmshftlem  21829  ulmshft  21830  ulmuni  21832  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmdvlem1  21840  ulmdvlem3  21842  mtest  21844  mtestbdd  21845  mbfulm  21846  itgulm  21848  itgulm2  21849  pserval2  21851  pserulm  21862  psercn  21866  pserdvlem2  21868  pserdv  21869  pige3  21954  logtayl  22080  rlimcnp  22334  sqff1o  22495  muinv  22508  dchrinv  22575  sumdchr2  22584  dchr2sum  22587  lgsval4  22630  lgsmod  22635  lgsqrlem1  22655  dchrmusumlema  22717  dchrvmasumlem1  22719  dchrisum0re  22737  dchrisum0lema  22738  logsqvma2  22767  padicval  22841  iscgrg  22940  midexlem  23051  brcgr  23097  ecgrtg  23180  vdgrfval  23516  vdgrval  23517  iseupa  23537  eupath2lem3  23551  eupath2  23552  grpoinvval  23663  grpodivfval  23680  gxfval  23695  gxval  23696  imsdval  24028  sspnval  24086  nmoofval  24113  nmooval  24114  bloval  24132  0oval  24139  nmlno0  24146  hmoval  24161  ajval  24213  ubth  24225  htthlem  24270  pjhval  24751  pjoc1  24788  pjoc2  24793  pjige0  25045  pjcjt2  25046  pjch  25048  pjsumi  25064  pjdsi  25066  pjds3i  25067  pjopyth  25074  pjnorm  25078  pjpyth  25079  pjnel  25080  hosval  25095  homval  25096  hodval  25097  hfsval  25098  hfmval  25099  braval  25299  kbval  25309  eigvalval  25315  leopg  25477  leoppos  25481  leoprf2  25482  leoprf  25483  elpjrn  25545  pj3cor1i  25564  strlem2  25606  hstrlem2  25614  fmptcof2  25930  offval2f  25934  resf1o  25981  fpwrelmap  25984  fmcncfil  26313  nmmulg  26349  zrhnm  26350  qqhval  26355  qqhcn  26372  ofcfval  26492  ofcfval3  26496  brfae  26616  omsval  26660  sitgval  26670  eulerpartlemsv1  26691  eulerpartlemsf  26694  eulerpartlemgvv  26711  eulerpartlemn  26716  sseqval  26723  sseqfv1  26724  sseqfv2  26729  fibp1  26736  dstrvval  26805  ballotleme  26831  ballotlemi  26835  plymulx0  26900  plymulx  26901  signstfv  26916  signstfvneq0  26925  signstfvc  26927  signstres  26928  signstfveq0  26930  lgamgulmlem2  26968  lgamgulmlem5  26971  lgamgulm2  26974  lgamcvglem  26978  subfacp1lem5  27024  kur14  27056  ptpcon  27074  cvmliftmolem1  27122  cvmliftlem5  27130  cvmliftlem7  27132  cvmliftlem15  27139  cvmlift2lem3  27146  cvmlift2lem4  27147  cvmlift2lem7  27150  cvmlift2lem9  27152  cvmlift2  27157  cvmliftphtlem  27158  cvmlift3lem2  27161  cvmlift3lem5  27164  cvmlift3lem6  27165  cvmlift3lem7  27166  cvmlift3lem9  27168  cvmlift3  27169  relexp0  27282  relexpsucr  27283  shftvalg  27346  prodeq2w  27376  prodeq2ii  27377  prodmo  27400  fprod  27405  fprodss  27412  bpolylem  28142  ftc2nc  28429  neibastop3  28536  tailval  28547  filnetlem4  28555  cocanfo  28564  f1ocan2fv  28574  upixp  28576  sdclem2  28591  rrncmslem  28684  ismrer1  28690  isnacs  28993  mzpsubst  29038  eldioph2  29053  pw2f1ocnv  29339  fnwe2lem2  29357  islnr3  29424  hbtlem1  29432  hbtlem2  29433  hbtlem7  29434  hbtlem4  29435  hbtlem5  29437  hbt  29439  dgrsub2  29444  dgrnznn  29445  mpaaeu  29460  mpaalem  29462  rgspnval  29478  flcidc  29484  cntzsdrg  29512  itgpowd  29543  addrfv  29678  subrfv  29679  mulvfv  29680  refsum2cnlem1  29712  fmuldfeqlem1  29716  fmuldfeq  29717  fmul01lt1lem1  29718  fmul01lt1lem2  29719  stoweidlem17  29765  stoweidlem20  29768  stoweidlem27  29775  stoweidlem31  29779  stoweidlem34  29782  stoweidlem44  29792  stoweidlem48  29796  stoweidlem59  29807  stirlinglem3  29824  stirlinglem15  29836  elovmpt3rab1  30116  ccatw2s1p1  30222  ccatw2s1p2  30223  ccat2s1fvw  30224  wwlkn  30269  wlkiswwlkfun  30302  wlkiswwlkinj  30303  wlkiswwlksur  30304  wlkiswwlkbij2  30306  clwwlkn  30383  isrgra  30496  rusgranumwlklem4  30523  vdfrgra0  30567  vdgfrgra0  30568  coe1sclmulval  30771  evl1at0  30772  evl1at1  30773  mat1dimscm  30794  pmatcollpw1lem3  30816  pmatcollpw1  30819  pmatcollpw2lem  30820  m1detdiag  30823  mdetdiaglem  30824  lincvalpr  30841  bnj1379  31711  bj-finsumval0  32426  lshpset  32463  lsatset  32475  lkrval  32573  eqlkr  32584  ldualvaddval  32616  ldualvsval  32623  ldualvsubval  32642  cmtfvalN  32695  isoml  32723  pmapval  33241  pclvalN  33374  polfvalN  33388  polvalN  33389  psubclsetN  33420  watfvalN  33476  watvalN  33477  ldilset  33593  ltrnfset  33601  ltrnset  33602  dilfsetN  33636  dilsetN  33637  trnfsetN  33639  trnsetN  33640  trlfset  33644  trlset  33645  trlval  33646  ltrnideq  33659  cdlemd8  33689  cdlemg1idlemN  34056  cdlemg1fvawlemN  34057  cdlemg2idN  34080  trlcoabs2N  34206  tgrpfset  34228  tgrpset  34229  tendofset  34242  tendoset  34243  erngfset  34283  erngset  34284  erngfset-rN  34291  erngset-rN  34292  cdlemi2  34303  cdlemj1  34305  cdlemk2  34316  cdlemk4  34318  cdlemk8  34322  cdlemkuu  34379  cdlemk31  34380  cdlemkuv2-3N  34383  cdlemk18-3N  34384  cdlemk22-3  34385  cdlemkfid2N  34407  cdlemkyu  34411  cdlemk19ylem  34414  cdlemk46  34432  cdlemk49  34435  cdlemk43N  34447  cdlemk19u1  34453  cdlemk19u  34454  dvafset  34488  dvaset  34489  dvaplusgv  34494  diaffval  34515  diafval  34516  diaval  34517  dvhfset  34565  dvhset  34566  dvhlveclem  34593  docaffvalN  34606  docafvalN  34607  docavalN  34608  djaffvalN  34618  djafvalN  34619  dibffval  34625  dibfval  34626  dibval  34627  dicffval  34659  dicfval  34660  dicval  34661  dicelvalN  34663  dicvaddcl  34675  dicvscacl  34676  cdlemn8  34689  cdlemn9  34690  dihordlem7b  34700  dihffval  34715  dihfval  34716  dihval  34717  dihopelvalcpre  34733  dihmeetlem1N  34775  dihglblem5apreN  34776  dihmeetlem4preN  34791  dihmeetlem13N  34804  dih1dimatlem0  34813  dochffval  34834  dochfval  34835  dochval  34836  djhffval  34881  djhfval  34882  lcfl7lem  34984  lclkrlem2k  35002  lclkrlem2u  35012  lcdfval  35073  lcdval  35074  lcdvaddval  35083  lcdvsval  35089  lcd0vvalN  35098  lcdvsubval  35103  lcdlsp  35106  mapdffval  35111  mapdfval  35112  mapdval  35113  hvmapffval  35243  hvmapfval  35244  hvmapval  35245  hvmapvalvalN  35246  hvmapidN  35247  hvmaplkr  35253  hdmap1ffval  35281  hdmap1fval  35282  hdmap1vallem  35283  hdmapffval  35314  hdmapfval  35315  hdmapval  35316  hdmapevec2  35324  hgmapffval  35373  hgmapfval  35374  hgmapval  35375  hdmaplna2  35398  hdmapglnm2  35399  hdmapinvlem3  35408  hlhilset  35422  hlhilipval  35437
  Copyright terms: Public domain W3C validator