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

Theorem fveq1d 5730
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 5727 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   ` cfv 5454
This theorem is referenced by:  fveq12d  5734  csbfv2g  5740  funssfv  5746  fvmptd  5810  fvmpt2d  5814  mpteqb  5819  fvmptt  5820  fmptco  5901  fvunsn  5925  fvsng  5927  fsnunfv  5933  f1ocnvfv1  6014  f1ocnvfv2  6015  fcof1  6020  fcofo  6021  ofval  6314  offval2  6322  ofrfval2  6323  caofinvl  6331  curry1val  6439  curry2val  6443  fnwelem  6461  rdg0g  6685  oav  6755  omv  6756  oev  6758  resixpfo  7100  pw2f1olem  7212  mapxpen  7273  xpmapenlem  7274  ordtypelem6  7492  ordtypelem7  7493  unwdomg  7552  cantnffval  7618  cantnfval  7623  cantnfres  7633  cantnfp1lem3  7636  fseqenlem1  7905  fseqenlem2  7906  iunfictbso  7995  dfac12lem1  8023  dfac12lem2  8024  dfac12r  8026  ackbij2lem3  8121  ituni0  8298  itunisuc  8299  itunitc1  8300  ituniiun  8302  hsmexlem2  8307  hsmexlem4  8309  iundom2g  8415  konigthlem  8443  konigth  8444  fpwwe2lem6  8510  fpwwe2lem9  8513  rpnnen1lem3  10602  rpnnen1lem5  10604  fseq1p1m1  11122  seqp1  11338  seqf1olem2  11363  seqf1o  11364  seqid  11368  seqz  11371  seqof  11380  seqof2  11381  bcval5  11609  bcn2  11610  hashf1lem1  11704  seqcoll  11712  s1fv  11760  swrdfv  11771  splfv1  11784  revfv  11795  shftcan1  11898  shftcan2  11899  climshft2  12376  isercoll2  12462  sumeq2w  12486  sumeq2ii  12487  cbvsum  12489  summo  12511  fsum  12514  fsumss  12519  fsumcvg2  12521  isumsplit  12620  rpnnen2lem1  12814  rpnnen2  12825  ruclem4  12833  sadfval  12964  smufval  12989  odzval  13177  1arithlem2  13292  vdwpc  13348  vdwlem6  13354  ramval  13376  setsid  13508  setsnid  13509  prdsval  13678  prdsplusgfval  13696  prdsmulrfval  13698  pwsvscaval  13717  imasval  13737  xpsc0  13785  xpsc1  13786  mrisval  13855  comfffval  13924  sectffval  13976  invinv  13995  oppcsect  13999  brssc  14014  issubc  14035  isfunc  14061  funcoppc  14072  idfuval  14073  idfu2  14075  idfu1  14077  idfucl  14078  cofuval  14079  cofu1  14081  cofu2  14083  cofuval2  14084  cofucl  14085  cofurid  14088  resfval  14089  resfval2  14090  funcres  14093  funcpropd  14097  isfull  14107  isnat  14144  fucco  14159  homafval  14184  idafval  14212  setcmon  14242  catcisolem  14261  catciso  14262  xpcval  14274  1stf1  14289  2ndf1  14292  1stfcl  14294  2ndfcl  14295  prfval  14296  prf2fval  14298  prf1st  14301  prf2nd  14302  1st2ndprf  14303  evlf2  14315  evlf2val  14316  evlfcl  14319  curfval  14320  curfpropd  14330  uncfval  14331  uncf2  14334  curfuncf  14335  diag11  14340  diag12  14341  diag2  14342  curf2ndf  14344  hofval  14349  hofcl  14356  yon11  14361  yon12  14362  yon2  14363  yonedalem4a  14372  yonedalem4b  14373  yonedalem4c  14374  yonedalem22  14375  yonedalem3b  14376  yonedainv  14378  yoniso  14382  lubval  14436  glbval  14441  joinfval  14444  meetfval  14451  isclat  14538  odumeet  14567  odujoin  14569  oduclatb  14571  poslubdg  14575  prdspjmhm  14766  pwsco1mhm  14769  gsumvalx  14774  gsumpropd  14776  gsumress  14777  gsumval2a  14782  grpsubfval  14847  grplactval  14886  grpsubpropd  14889  grpsubpropd2  14890  mulgfval  14891  mulgpropd  14923  submmulg  14925  pwsinvg  14930  subgmulg  14958  eqgfval  14988  lactghmga  15107  symgga  15109  cntrval  15118  cntzval  15120  cntzrcl  15126  oppgsubg  15159  ispgp  15226  vrgpval  15399  frgpup3lem  15409  frgpnabllem1  15484  frgpnabllem2  15485  gsumval3eu  15513  gsumval3  15514  gsumzres  15517  gsumzf1o  15519  gsumzaddlem  15526  gsumconst  15532  dmdprd  15559  dprdval  15561  dmdprdsplitlem  15595  dprd2da  15600  dpjfval  15613  dpjidcl  15616  dpjlid  15619  dpjrid  15620  dvrfval  15789  staffval  15935  srngnvl  15944  issrngd  15949  lspval  16051  islbs  16148  lbspropd  16171  lssacsex  16216  lbsacsbs  16228  sralem  16249  srasca  16253  sravsca  16254  rlmval  16264  lpival  16316  aspval  16387  psrmulval  16450  psrvscaval  16456  psrdi  16470  psrdir  16471  mvrval  16485  mvrval2  16486  mvrf1  16489  mplsubglem  16498  mplvscaval  16511  subrgmvrf  16525  opsrle  16536  opsrbaslem  16538  subrgasclcl  16559  psr1val  16584  vr1val  16590  coe1fv  16604  subrgvr1  16654  coe1addfv  16658  coe1subfv  16659  coe1tmfv1  16666  coe1tmfv2  16667  coe1tmmul2fv  16670  coe1pwmulfv  16672  coe1sclmulfv  16675  ply1sclid  16679  ply1sclf1  16680  zrhmulg  16791  chrval  16806  chrrhm  16812  znzrhval  16827  ocvval  16894  elocv  16895  cssval  16909  pjfval  16933  pjfo  16942  isobs  16947  ntrval  17100  clsval  17101  opncldf3  17150  neival  17166  neiptopreu  17197  lpfval  17202  lpval  17203  cnpval  17300  iscnp2  17303  isreg  17396  isnrm  17399  2ndcsep  17522  isnlly  17532  ptval  17602  dfac14  17650  cnmptk2  17718  pt1hmeo  17838  xkocnv  17846  fmval  17975  ufldom  17994  flimval  17995  flffval  18021  flfval  18022  cnpflf  18033  txflf  18038  fclsval  18040  fcfval  18065  cnextval  18092  cnextfvval  18096  cnextcn  18098  cnextfres  18099  symgtgp  18131  tgpconcomp  18142  prdstmdd  18153  utopsnneiplem  18277  neipcfilu  18326  txmetcnp  18577  subgnm2  18675  tngngp  18695  isnlm  18711  sranlm  18720  lssnlm  18736  nmofval  18748  nmoval  18749  isphtpy  19006  pcovalg  19037  pco1  19040  clmneg  19106  clmabs  19107  nmoleub2lem3  19123  nmoleub3  19127  cphcjcl  19146  cphnm  19156  cphipcj  19162  cphassr  19174  tchnmval  19187  tchcphlem3  19190  ipcau2  19191  tchcphlem1  19192  tchcphlem2  19193  tchcph  19194  ipcau  19195  ovolctb  19386  voliunlem3  19446  uniioombllem2  19475  vitalilem4  19503  mbflimsup  19558  itg1climres  19606  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  mbfi1flimlem  19614  mbfmullem2  19616  mbfmullem  19617  itg2monolem1  19642  itg2mono  19645  itg2i1fseqle  19646  itg2i1fseq  19647  itg2addlem  19650  itg2cnlem1  19653  limcfval  19759  limcmpt2  19771  limcres  19773  cnplimc  19774  dvfval  19784  dvreslem  19796  dvres2lem  19797  dvn0  19810  dvnp1  19811  cpnfval  19818  elcpn  19820  dvaddbr  19824  dvmulbr  19825  dvcmul  19830  dvfre  19837  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  dvlip2  19879  c1liplem1  19880  dveq0  19884  dv11cn  19885  dvivthlem1  19892  dvivth  19894  dvne0  19895  lhop1lem  19897  lhop2  19899  lhop  19900  dvcnvrelem2  19902  dvcvx  19904  dvfsumabs  19907  ftc1lem6  19925  ftc2  19928  ftc2ditglem  19929  itgparts  19931  itgsubstlem  19932  evlslem1  19936  evlsval  19940  evlssca  19943  evlsvar  19944  evlval  19945  evl1sca  19950  evl1scad  19951  evl1var  19952  evl1vard  19953  evl1addd  19954  evl1subd  19955  evl1muld  19956  evl1vsd  19957  evl1expd  19958  pf1ind  19975  mdegaddle  19997  mdegmullem  20001  coe1mul3  20022  uc1pval  20062  mon1pval  20064  uc1pmon1p  20074  q1pval  20076  ply1remlem  20085  ply1rem  20086  fta1glem2  20089  fta1g  20090  fta1blem  20091  ig1pval  20095  plyeq0lem  20129  coeeulem  20143  coeid2  20158  dgrle  20162  dgreq  20163  0dgrb  20165  coemul  20170  coe11  20171  coe1term  20177  dgrlt  20184  dgradd2  20186  dgrcolem2  20192  plymul0or  20198  plydivlem4  20213  plydiveu  20215  plyremlem  20221  plyrem  20222  fta1  20225  vieta1lem2  20228  plyexmo  20230  aareccl  20243  aannenlem1  20245  aannenlem2  20246  taylfval  20275  tayl0  20278  dvtaylp  20286  dvntaylp0  20288  taylthlem1  20289  taylthlem2  20290  ulmval  20296  ulmres  20304  ulmshftlem  20305  ulmshft  20306  ulmuni  20308  ulmcaulem  20310  ulmcau  20311  ulmss  20313  ulmdvlem1  20316  ulmdvlem3  20318  mtest  20320  mtestbdd  20321  mbfulm  20322  itgulm  20324  itgulm2  20325  pserval2  20327  pserulm  20338  psercn  20342  pserdvlem2  20344  pserdv  20345  pige3  20425  logtayl  20551  rlimcnp  20804  sqff1o  20965  muinv  20978  dchrinv  21045  sumdchr2  21054  dchr2sum  21057  lgsval4  21100  lgsmod  21105  lgsqrlem1  21125  dchrmusumlema  21187  dchrvmasumlem1  21189  dchrisum0re  21207  dchrisum0lema  21208  logsqvma2  21237  padicval  21311  vdgrfval  21666  vdgrval  21667  iseupa  21687  eupath2lem3  21701  eupath2  21702  grpoinvval  21813  grpodivfval  21830  gxfval  21845  gxval  21846  imsdval  22178  sspnval  22236  nmoofval  22263  nmooval  22264  bloval  22282  0oval  22289  nmlno0  22296  hmoval  22311  ajval  22363  ubth  22375  htthlem  22420  pjhval  22899  pjoc1  22936  pjoc2  22941  pjige0  23193  pjcjt2  23194  pjch  23196  pjsumi  23212  pjdsi  23214  pjds3i  23215  pjopyth  23222  pjnorm  23226  pjpyth  23227  pjnel  23228  hosval  23243  homval  23244  hodval  23245  hfsval  23246  hfmval  23247  braval  23447  kbval  23457  eigvalval  23463  leopg  23625  leoppos  23629  leoprf2  23630  leoprf  23631  elpjrn  23693  pj3cor1i  23712  strlem2  23754  hstrlem2  23762  fmptcof2  24076  offval2f  24080  fmcncfil  24317  nmmulg  24352  zrhnm  24353  qqhval  24358  qqhcn  24375  ofcfval  24481  ofcfval3  24485  brfae  24599  sitgval  24647  dstrvval  24728  ballotleme  24754  ballotlemi  24758  lgamgulmlem2  24814  lgamgulmlem5  24817  lgamgulm2  24820  lgamcvglem  24824  subfacp1lem5  24870  kur14  24902  ptpcon  24920  cvmliftmolem1  24968  cvmliftlem5  24976  cvmliftlem7  24978  cvmliftlem15  24985  cvmlift2lem3  24992  cvmlift2lem4  24993  cvmlift2lem7  24996  cvmlift2lem9  24998  cvmlift2  25003  cvmliftphtlem  25004  cvmlift3lem2  25007  cvmlift3lem5  25010  cvmlift3lem6  25011  cvmlift3lem7  25012  cvmlift3lem9  25014  cvmlift3  25015  relexp0  25129  relexpsucr  25130  shftvalg  25208  prodeq2w  25238  prodeq2ii  25239  prodmo  25262  fprod  25267  fprodss  25274  brcgr  25839  bpolylem  26094  ftc2nc  26289  neibastop3  26391  tailval  26402  filnetlem4  26410  cocanfo  26419  f1ocan2fv  26429  upixp  26431  sdclem2  26446  rrncmslem  26541  ismrer1  26547  isnacs  26758  mzpsubst  26805  eldioph2  26820  pw2f1ocnv  27108  fnwe2lem2  27126  dsmmval  27177  dsmm0cl  27183  prdsinvgd2  27185  frlmvscaval  27208  uvcval  27211  uvcvval  27212  uvcresum  27219  islnr3  27296  hbtlem1  27304  hbtlem2  27305  hbtlem7  27306  hbtlem4  27307  hbtlem5  27309  hbt  27311  dgrsub2  27316  dgrnznn  27317  mpaaeu  27332  mpaalem  27334  rgspnval  27350  flcidc  27356  pmtrval  27371  pmtrfv  27372  pmtrffv  27378  mdetfval  27464  cntzsdrg  27487  addrfv  27650  subrfv  27651  mulvfv  27652  refsum2cnlem1  27684  fmuldfeqlem1  27688  fmuldfeq  27689  fmul01lt1lem1  27690  fmul01lt1lem2  27691  stoweidlem17  27742  stoweidlem20  27745  stoweidlem27  27752  stoweidlem31  27756  stoweidlem34  27759  stoweidlem42  27767  stoweidlem44  27769  stoweidlem48  27773  stoweidlem59  27784  stirlinglem3  27801  stirlinglem15  27813  swrdswrd  28199  cshwidx  28242  isrgra  28369  vdfrgra0  28412  vdgfrgra0  28413  bnj1379  29202  lshpset  29776  lsatset  29788  lkrval  29886  eqlkr  29897  ldualvaddval  29929  ldualvsval  29936  ldualvsubval  29955  cmtfvalN  30008  isoml  30036  pmapval  30554  pclvalN  30687  polfvalN  30701  polvalN  30702  psubclsetN  30733  watfvalN  30789  watvalN  30790  ldilset  30906  ltrnfset  30914  ltrnset  30915  dilfsetN  30949  dilsetN  30950  trnfsetN  30952  trnsetN  30953  trlfset  30957  trlset  30958  trlval  30959  ltrnideq  30972  cdlemd8  31002  cdlemg1idlemN  31369  cdlemg1fvawlemN  31370  cdlemg2idN  31393  trlcoabs2N  31519  tgrpfset  31541  tgrpset  31542  tendofset  31555  tendoset  31556  erngfset  31596  erngset  31597  erngfset-rN  31604  erngset-rN  31605  cdlemi2  31616  cdlemj1  31618  cdlemk2  31629  cdlemk4  31631  cdlemk8  31635  cdlemkuu  31692  cdlemk31  31693  cdlemkuv2-3N  31696  cdlemk18-3N  31697  cdlemk22-3  31698  cdlemkfid2N  31720  cdlemkyu  31724  cdlemk19ylem  31727  cdlemk46  31745  cdlemk49  31748  cdlemk43N  31760  cdlemk19u1  31766  cdlemk19u  31767  dvafset  31801  dvaset  31802  dvaplusgv  31807  diaffval  31828  diafval  31829  diaval  31830  dvhfset  31878  dvhset  31879  dvhlveclem  31906  docaffvalN  31919  docafvalN  31920  docavalN  31921  djaffvalN  31931  djafvalN  31932  dibffval  31938  dibfval  31939  dibval  31940  dicffval  31972  dicfval  31973  dicval  31974  dicelvalN  31976  dicvaddcl  31988  dicvscacl  31989  cdlemn8  32002  cdlemn9  32003  dihordlem7b  32013  dihffval  32028  dihfval  32029  dihval  32030  dihopelvalcpre  32046  dihmeetlem1N  32088  dihglblem5apreN  32089  dihmeetlem4preN  32104  dihmeetlem13N  32117  dih1dimatlem0  32126  dochffval  32147  dochfval  32148  dochval  32149  djhffval  32194  djhfval  32195  lcfl7lem  32297  lclkrlem2k  32315  lclkrlem2u  32325  lcdfval  32386  lcdval  32387  lcdvaddval  32396  lcdvsval  32402  lcd0vvalN  32411  lcdvsubval  32416  lcdlsp  32419  mapdffval  32424  mapdfval  32425  mapdval  32426  hvmapffval  32556  hvmapfval  32557  hvmapval  32558  hvmapvalvalN  32559  hvmapidN  32560  hvmaplkr  32566  hdmap1ffval  32594  hdmap1fval  32595  hdmap1vallem  32596  hdmapffval  32627  hdmapfval  32628  hdmapval  32629  hdmapevec2  32637  hgmapffval  32686  hgmapfval  32687  hgmapval  32688  hdmaplna2  32711  hdmapglnm2  32712  hdmapinvlem3  32721  hlhilset  32735  hlhilipval  32750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462
  Copyright terms: Public domain W3C validator