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

Theorem fveq1d 5866
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 5863 . 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 1379   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594
This theorem is referenced by:  fveq12d  5870  funssfv  5879  csbfv12  5899  csbfv2g  5901  fvmptd  5953  fvmpt2d  5957  mpteqb  5962  fvmptt  5963  fnmptfvd  5982  fmptco  6052  fvunsn  6091  fvsng  6093  fsnunfv  6099  f1ocnvfv1  6168  f1ocnvfv2  6169  fcof1  6176  fcofo  6177  csbov123  6313  elovmpt3rab1  6518  ofval  6531  offval2  6538  ofrfval2  6539  caofinvl  6549  curry1val  6873  curry2val  6877  fnwelem  6895  fvmpt2curryd  6997  rdg0g  7090  oav  7158  omv  7159  oev  7161  resixpfo  7504  pw2f1olem  7618  mapxpen  7680  xpmapenlem  7681  ordtypelem6  7944  ordtypelem7  7945  unwdomg  8006  cantnffval  8076  cantnfval  8083  cantnfres  8092  cantnfp1lem3  8095  cantnfvalOLD  8113  cantnfp1lem3OLD  8121  fseqenlem1  8401  fseqenlem2  8402  iunfictbso  8491  dfac12lem1  8519  dfac12lem2  8520  dfac12r  8522  ackbij2lem3  8617  ituni0  8794  itunisuc  8795  itunitc1  8796  ituniiun  8798  hsmexlem2  8803  hsmexlem4  8805  iundom2g  8911  konigthlem  8939  konigth  8940  fpwwe2lem6  9009  fpwwe2lem9  9012  rpnnen1lem3  11206  rpnnen1lem5  11208  fseq1p1m1  11748  seqp1  12085  seqf1olem2  12110  seqf1o  12111  seqid  12115  seqz  12118  seqof  12127  seqof2  12128  bcval5  12358  bcn2  12359  hashf1lem1  12464  seqcoll  12472  s1fv  12576  ccatw2s1p1  12597  ccatw2s1p2  12598  swrdfv  12608  swrdswrd  12642  splfv1  12688  revfv  12694  cshwidxmod  12731  ccat2s1fvwALT  12850  shftcan1  12873  shftcan2  12874  climshft2  13361  isercoll2  13447  sumeq2w  13470  sumeq2ii  13471  summo  13495  fsum  13498  fsumss  13503  fsumcvg2  13505  isumsplit  13608  rpnnen2lem1  13802  rpnnen2  13813  ruclem4  13821  sadfval  13954  smufval  13979  odzval  14170  1arithlem2  14294  vdwpc  14350  vdwlem6  14356  ramval  14378  fvsetsid  14508  setsid  14524  setsnid  14525  prdsval  14703  prdsplusgfval  14722  prdsmulrfval  14724  pwsvscaval  14743  imasval  14759  xpsc0  14808  xpsc1  14809  mrisval  14878  comfffval  14947  sectffval  14999  invinv  15018  oppcsect  15022  brssc  15037  issubc  15058  isfunc  15084  funcoppc  15095  idfuval  15096  idfu2  15098  idfu1  15100  idfucl  15101  cofuval  15102  cofu1  15104  cofu2  15106  cofuval2  15107  cofucl  15108  cofurid  15111  resfval  15112  resfval2  15113  funcres  15116  funcpropd  15120  isfull  15130  isnat  15167  fucco  15182  homafval  15207  idafval  15235  setcmon  15265  catcisolem  15284  catciso  15285  xpcval  15297  1stf1  15312  2ndf1  15315  1stfcl  15317  2ndfcl  15318  prfval  15319  prf2fval  15321  prf1st  15324  prf2nd  15325  1st2ndprf  15326  evlf2  15338  evlf2val  15339  evlfcl  15342  curfval  15343  curfpropd  15353  uncfval  15354  uncf2  15357  curfuncf  15358  diag11  15363  diag12  15364  diag2  15365  curf2ndf  15367  hofval  15372  hofcl  15379  yon11  15384  yon12  15385  yon2  15386  yonedalem4a  15395  yonedalem4b  15396  yonedalem4c  15397  yonedalem22  15398  yonedalem3b  15399  yonedainv  15401  yoniso  15405  lubval  15464  glbval  15477  poslubdg  15629  prdspjmhm  15805  pwsco1mhm  15808  gsumvalx  15812  gsumpropd  15814  gsumress  15817  gsumval2a  15822  grpsubfval  15890  grplactval  15935  grpsubpropd  15938  grpsubpropd2  15939  mulgfval  15940  mulgpropd  15972  submmulg  15974  pwsinvg  15979  subgmulg  16007  eqgfval  16041  cntrval  16149  cntzval  16151  cntzrcl  16157  oppgsubg  16190  lactghmga  16221  symgga  16223  gsmsymgrfixlem1  16244  gsmsymgrfix  16245  gsmsymgreqlem1  16247  gsmsymgreqlem2  16248  gsmsymgreq  16249  pmtrval  16269  pmtrfv  16270  pmtrffv  16277  pmtrdifwrdellem3  16301  pmtrdifwrdel2lem1  16302  pmtrdifwrdel  16303  pmtrdifwrdel2  16304  ispgp  16405  vrgpval  16578  frgpup3lem  16588  frgpnabllem1  16665  frgpnabllem2  16666  gsumval3eu  16695  gsumval3OLD  16696  gsumval3lem2  16698  gsumval3  16699  gsumzres  16702  gsumzf1o  16705  gsumzresOLD  16706  gsumzf1oOLD  16708  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  dmdprd  16817  dprdval  16822  dprdvalOLD  16824  dmdprdsplitlem  16871  dmdprdsplitlemOLD  16872  dprd2da  16878  dpjfval  16891  dpjidcl  16894  dpjlid  16897  dpjrid  16898  dpjidclOLD  16901  dvrfval  17114  staffval  17276  srngnvl  17285  issrngd  17290  lspval  17401  islbs  17502  lbspropd  17525  lssacsex  17570  lbsacsbs  17582  sralem  17603  srasca  17607  sravsca  17608  sraip  17609  rlmval  17617  ixpsnbasval  17635  lpival  17672  rrgsupp  17707  aspval  17745  psrmulval  17807  psrvscaval  17813  psrdi  17829  psrdir  17830  mvrval  17845  mvrval2  17846  mvrf1  17849  mplsubglem  17861  mplsubglemOLD  17863  mplvscaval  17878  subrgmvrf  17892  opsrle  17908  opsrbaslem  17910  subrgasclcl  17932  evlslem1  17952  evlsval  17956  evlssca  17959  evlsvar  17960  evlval  17961  evlsscasrng  17963  evlsvarsrng  17965  evlvar  17966  psr1val  17993  vr1val  17999  coe1fv  18013  subrgvr1  18070  coe1addfv  18074  coe1subfv  18075  coe1tmfv1  18083  coe1tmfv2  18084  coe1tmmul2fv  18087  coe1pwmulfv  18089  coe1sclmulfv  18092  ply1sclid  18097  ply1sclf1  18098  ply1coe1eq  18108  cply1coe0bi  18110  coe1fzgsumdlem  18111  coe1fzgsumd  18112  gsummoncoe1  18114  gsumply1eq  18115  evls1val  18125  evls1sca  18128  evl1sca  18138  evl1scad  18139  evl1var  18140  evl1vard  18141  evls1var  18142  evls1scasrng  18143  evls1varsrng  18144  evl1addd  18145  evl1subd  18146  evl1muld  18147  evl1vsd  18148  evl1expd  18149  pf1ind  18159  evl1gsumdlem  18160  evl1gsumd  18161  evl1gsumadd  18162  zrhmulg  18311  chrval  18326  chrrhm  18332  znzrhval  18349  psgndiflemA  18401  ocvval  18462  elocv  18463  cssval  18477  pjfval  18501  pjfo  18510  isobs  18515  dsmmval  18529  dsmm0cl  18535  prdsinvgd2  18537  frlmvscaval  18564  frlmphl  18576  uvcval  18580  uvcvval  18581  uvcresum  18588  mat1dimscm  18741  mat1rhmelval  18746  marepvval  18833  mdetfval  18852  mdetleib2  18854  mdet0fv0  18860  m1detdiag  18863  mdetdiaglem  18864  mdetralt  18874  mdetunilem7  18884  mdetuni0  18887  m2detleiblem1  18890  smadiadetr  18941  cramerimplem1  18949  cpmatel  18976  1elcpmat  18980  cpmatinvcl  18982  cpmatmcllem  18983  cpmatmcl  18984  mat2pmatfval  18988  m2cpm  19006  cpm2mval  19015  cpm2mvalel  19016  m2cpminvid  19018  m2cpminvid2lem  19019  m2cpminvid2  19020  m2cpmfo  19021  decpmate  19031  decpmatid  19035  decpmatmullem  19036  decpmatmulsumfsupp  19038  monmatcollpw  19044  pmatcollpw3lem  19048  pmatcollpwscmatlem1  19054  pmatcollpwscmatlem2  19055  pm2mpf1  19064  pm2mpcoe1  19065  mply1topmatval  19069  mp2pm2mplem1  19071  mp2pm2mplem3  19073  mp2pm2mplem4  19074  mp2pm2mp  19076  pm2mpghm  19081  pm2mpmhmlem1  19083  pm2mpmhmlem2  19084  chpmatfval  19095  chpmat0d  19099  chpscmatgsumbin  19109  cayleyhamilton0  19154  cayleyhamiltonALT  19156  ntrval  19300  clsval  19301  opncldf3  19350  neival  19366  neiptopreu  19397  lpfval  19402  lpval  19403  cnpval  19500  iscnp2  19503  isreg  19596  isnrm  19599  2ndcsep  19723  isnlly  19733  ptval  19803  dfac14  19851  cnmptk2  19919  pt1hmeo  20039  xkocnv  20047  fmval  20176  ufldom  20195  flimval  20196  flffval  20222  flfval  20223  cnpflf  20234  txflf  20239  fclsval  20241  fcfval  20266  cnextval  20293  cnextfvval  20297  cnextcn  20299  cnextfres  20300  symgtgp  20332  tgpconcomp  20343  prdstmdd  20354  utopsnneiplem  20482  neipcfilu  20531  txmetcnp  20782  subgnm2  20880  tngngp  20900  isnlm  20916  sranlm  20925  lssnlm  20941  nmofval  20953  nmoval  20954  isphtpy  21213  pcovalg  21244  pco1  21247  clmneg  21313  clmabs  21314  nmoleub2lem3  21330  nmoleub3  21334  cphcjcl  21362  cphnm  21372  cphipcj  21378  cphassr  21390  tchnmval  21404  tchcphlem3  21408  ipcau2  21409  tchcphlem1  21410  tchcphlem2  21411  tchcph  21412  ipcau  21413  rrxnm  21555  ovolctb  21633  voliunlem3  21694  uniioombllem2  21724  vitalilem4  21752  mbflimsup  21805  itg1climres  21853  mbfi1fseqlem4  21857  mbfi1fseqlem5  21858  mbfi1fseqlem6  21859  mbfi1flimlem  21861  mbfmullem2  21863  mbfmullem  21864  itg2monolem1  21889  itg2mono  21892  itg2i1fseqle  21893  itg2i1fseq  21894  itg2addlem  21897  itg2cnlem1  21900  limcfval  22008  limcmpt2  22020  limcres  22022  cnplimc  22023  dvfval  22033  dvreslem  22045  dvres2lem  22046  dvn0  22059  dvnp1  22060  cpnfval  22067  elcpn  22069  dvaddbr  22073  dvmulbr  22074  dvcmul  22079  dvfre  22086  rolle  22123  cmvth  22124  mvth  22125  dvlip  22126  dvlipcn  22127  dvlip2  22128  c1liplem1  22129  dveq0  22133  dv11cn  22134  dvivthlem1  22141  dvivth  22143  dvne0  22144  lhop1lem  22146  lhop2  22148  lhop  22149  dvcnvrelem2  22151  dvcvx  22153  dvfsumabs  22156  ftc1lem6  22174  ftc2  22177  ftc2ditglem  22178  itgparts  22180  itgsubstlem  22181  mdegaddle  22206  mdegmullem  22210  coe1mul3  22232  uc1pval  22272  mon1pval  22274  uc1pmon1p  22284  q1pval  22286  ply1remlem  22295  ply1rem  22296  fta1glem2  22299  fta1g  22300  fta1blem  22301  ig1pval  22305  plyeq0lem  22339  coeeulem  22353  coeid2  22368  dgrle  22372  dgreq  22373  0dgrb  22375  coemul  22380  coe11  22381  coe1term  22387  dgrlt  22394  dgradd2  22396  dgrcolem2  22402  plymul0or  22408  plydivlem4  22423  plydiveu  22425  plyremlem  22431  plyrem  22432  fta1  22435  vieta1lem2  22438  plyexmo  22440  aareccl  22453  aannenlem1  22455  aannenlem2  22456  taylfval  22485  tayl0  22488  dvtaylp  22496  dvntaylp0  22498  taylthlem1  22499  taylthlem2  22500  ulmval  22506  ulmres  22514  ulmshftlem  22515  ulmshft  22516  ulmuni  22518  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmdvlem1  22526  ulmdvlem3  22528  mtest  22530  mtestbdd  22531  mbfulm  22532  itgulm  22534  itgulm2  22535  pserval2  22537  pserulm  22548  psercn  22552  pserdvlem2  22554  pserdv  22555  pige3  22640  logtayl  22766  rlimcnp  23020  sqff1o  23181  muinv  23194  dchrinv  23261  sumdchr2  23270  dchr2sum  23273  lgsval4  23316  lgsmod  23321  lgsqrlem1  23341  dchrmusumlema  23403  dchrvmasumlem1  23405  dchrisum0re  23423  dchrisum0lema  23424  logsqvma2  23453  padicval  23527  iscgrg  23629  midexlem  23774  colperpexlem2  23807  colperpexlem3  23808  mideulem  23810  mideu  23811  midf  23816  ismidb  23818  lmieu  23824  lmimid  23833  brcgr  23876  ecgrtg  23959  wwlkn  24355  wlkiswwlkfun  24390  wlkiswwlkinj  24391  wlkiswwlksur  24392  wlkiswwlkbij2  24394  clwwlkn  24440  vdgrfval  24568  vdgrval  24569  isrgra  24599  isrgrac  24607  rusgranumwlklem4  24625  iseupa  24638  eupath2lem3  24652  eupath2  24653  vdfrgra0  24695  vdgfrgra0  24696  grpoinvval  24900  grpodivfval  24917  gxfval  24932  gxval  24933  imsdval  25265  sspnval  25323  nmoofval  25350  nmooval  25351  bloval  25369  0oval  25376  nmlno0  25383  hmoval  25398  ajval  25450  ubth  25462  htthlem  25507  pjhval  25988  pjoc1  26025  pjoc2  26030  pjige0  26282  pjcjt2  26283  pjch  26285  pjsumi  26301  pjdsi  26303  pjds3i  26304  pjopyth  26311  pjnorm  26315  pjpyth  26316  pjnel  26317  hosval  26332  homval  26333  hodval  26334  hfsval  26335  hfmval  26336  braval  26536  kbval  26546  eigvalval  26552  leopg  26714  leoppos  26718  leoprf2  26719  leoprf  26720  elpjrn  26782  pj3cor1i  26801  strlem2  26843  hstrlem2  26851  fmptcof2  27171  offval2f  27175  resf1o  27222  fpwrelmap  27225  fmcncfil  27546  nmmulg  27582  zrhnm  27583  qqhval  27588  qqhcn  27605  ofcfval  27734  ofcfval3  27738  brfae  27857  omsval  27901  sitgval  27911  eulerpartlemsv1  27932  eulerpartlemsf  27935  eulerpartlemgvv  27952  eulerpartlemn  27957  sseqval  27964  sseqfv1  27965  sseqfv2  27970  fibp1  27977  dstrvval  28046  ballotleme  28072  ballotlemi  28076  plymulx0  28141  plymulx  28142  signstfv  28157  signstfvneq0  28166  signstfvc  28168  signstres  28169  signstfveq0  28171  lgamgulmlem2  28209  lgamgulmlem5  28212  lgamgulm2  28215  lgamcvglem  28219  subfacp1lem5  28265  kur14  28297  ptpcon  28315  cvmliftmolem1  28363  cvmliftlem5  28371  cvmliftlem7  28373  cvmliftlem15  28380  cvmlift2lem3  28387  cvmlift2lem4  28388  cvmlift2lem7  28391  cvmlift2lem9  28393  cvmlift2  28398  cvmliftphtlem  28399  cvmlift3lem2  28402  cvmlift3lem5  28405  cvmlift3lem6  28406  cvmlift3lem7  28407  cvmlift3lem9  28409  cvmlift3  28410  relexp0  28524  relexpsucr  28525  shftvalg  28588  prodeq2w  28618  prodeq2ii  28619  prodmo  28642  fprod  28647  fprodss  28654  bpolylem  29384  ftc2nc  29674  neibastop3  29781  tailval  29792  filnetlem4  29800  cocanfo  29809  f1ocan2fv  29819  upixp  29821  sdclem2  29836  rrncmslem  29929  ismrer1  29935  isnacs  30238  mzpsubst  30283  eldioph2  30297  pw2f1ocnv  30583  fnwe2lem2  30601  islnr3  30668  hbtlem1  30676  hbtlem2  30677  hbtlem7  30678  hbtlem4  30679  hbtlem5  30681  hbt  30683  dgrsub2  30688  dgrnznn  30689  mpaaeu  30704  mpaalem  30706  rgspnval  30722  flcidc  30728  cntzsdrg  30756  itgpowd  30787  addrfv  30956  subrfv  30957  mulvfv  30958  refsum2cnlem1  30990  fvmpt2bd  31024  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  limciccioolb  31163  limcicciooub  31179  cncfuni  31225  cncficcgt0  31227  cncfiooicclem1  31232  dvsinax  31241  dvdivbd  31253  dvbdfbdioolem1  31258  itgsincmulx  31292  stoweidlem17  31317  stoweidlem20  31320  stoweidlem27  31327  stoweidlem31  31331  stoweidlem34  31334  stoweidlem44  31344  stoweidlem48  31348  stoweidlem59  31359  stirlinglem3  31376  stirlinglem15  31388  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem3  31405  dirkercncflem4  31406  dirkercncf  31407  fourierdlem42  31449  fourierdlem60  31467  fourierdlem61  31468  fourierdlem68  31475  fourierdlem73  31480  fourierdlem80  31487  fourierdlem93  31500  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  coe1sclmulval  32058  ply1mulgsum  32063  evl1at0  32064  evl1at1  32065  lincvalpr  32092  bnj1379  32968  bj-finsumval0  33735  lshpset  33775  lsatset  33787  lkrval  33885  eqlkr  33896  ldualvaddval  33928  ldualvsval  33935  ldualvsubval  33954  cmtfvalN  34007  isoml  34035  pmapval  34553  pclvalN  34686  polfvalN  34700  polvalN  34701  psubclsetN  34732  watfvalN  34788  watvalN  34789  ldilset  34905  ltrnfset  34913  ltrnset  34914  dilfsetN  34948  dilsetN  34949  trnfsetN  34951  trnsetN  34952  trlfset  34956  trlset  34957  trlval  34958  ltrnideq  34971  cdlemd8  35001  cdlemg1idlemN  35368  cdlemg1fvawlemN  35369  cdlemg2idN  35392  trlcoabs2N  35518  tgrpfset  35540  tgrpset  35541  tendofset  35554  tendoset  35555  erngfset  35595  erngset  35596  erngfset-rN  35603  erngset-rN  35604  cdlemi2  35615  cdlemj1  35617  cdlemk2  35628  cdlemk4  35630  cdlemk8  35634  cdlemkuu  35691  cdlemk31  35692  cdlemkuv2-3N  35695  cdlemk18-3N  35696  cdlemk22-3  35697  cdlemkfid2N  35719  cdlemkyu  35723  cdlemk19ylem  35726  cdlemk46  35744  cdlemk49  35747  cdlemk43N  35759  cdlemk19u1  35765  cdlemk19u  35766  dvafset  35800  dvaset  35801  dvaplusgv  35806  diaffval  35827  diafval  35828  diaval  35829  dvhfset  35877  dvhset  35878  dvhlveclem  35905  docaffvalN  35918  docafvalN  35919  docavalN  35920  djaffvalN  35930  djafvalN  35931  dibffval  35937  dibfval  35938  dibval  35939  dicffval  35971  dicfval  35972  dicval  35973  dicelvalN  35975  dicvaddcl  35987  dicvscacl  35988  cdlemn8  36001  cdlemn9  36002  dihordlem7b  36012  dihffval  36027  dihfval  36028  dihval  36029  dihopelvalcpre  36045  dihmeetlem1N  36087  dihglblem5apreN  36088  dihmeetlem4preN  36103  dihmeetlem13N  36116  dih1dimatlem0  36125  dochffval  36146  dochfval  36147  dochval  36148  djhffval  36193  djhfval  36194  lcfl7lem  36296  lclkrlem2k  36314  lclkrlem2u  36324  lcdfval  36385  lcdval  36386  lcdvaddval  36395  lcdvsval  36401  lcd0vvalN  36410  lcdvsubval  36415  lcdlsp  36418  mapdffval  36423  mapdfval  36424  mapdval  36425  hvmapffval  36555  hvmapfval  36556  hvmapval  36557  hvmapvalvalN  36558  hvmapidN  36559  hvmaplkr  36565  hdmap1ffval  36593  hdmap1fval  36594  hdmap1vallem  36595  hdmapffval  36626  hdmapfval  36627  hdmapval  36628  hdmapevec2  36636  hgmapffval  36685  hgmapfval  36686  hgmapval  36687  hdmaplna2  36710  hdmapglnm2  36711  hdmapinvlem3  36720  hlhilset  36734  hlhilipval  36749
  Copyright terms: Public domain W3C validator