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

Theorem fveq1d 5488
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 5485 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2syl 15 1  |-  ( ph  ->  ( F `  A
)  =  ( G `
 A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   ` cfv 5221
This theorem is referenced by:  fveq12d  5492  csbfv2g  5498  funssfv  5504  fvmptd  5568  mpteqb  5576  fvmptt  5577  fmptco  5653  fvunsn  5674  fvsng  5676  fsnunfv  5682  f1ocnvfv1  5754  f1ocnvfv2  5755  fcof1  5759  fcofo  5760  ofval  6049  offval2  6057  ofrfval2  6058  caofinvl  6066  curry1val  6173  curry2val  6177  fnwelem  6192  rdg0g  6436  oav  6506  omv  6507  oev  6509  resixpfo  6850  pw2f1olem  6962  mapxpen  7023  xpmapenlem  7024  ordtypelem6  7234  ordtypelem7  7235  unwdomg  7294  cantnffval  7360  cantnfval  7365  cantnfres  7375  cantnfp1lem3  7378  fseqenlem1  7647  fseqenlem2  7648  iunfictbso  7737  dfac12lem1  7765  dfac12lem2  7766  dfac12r  7768  ackbij2lem3  7863  ituni0  8040  itunisuc  8041  itunitc1  8042  ituniiun  8044  hsmexlem2  8049  hsmexlem4  8051  iundom2g  8158  konigthlem  8186  konigth  8187  fpwwe2lem6  8253  fpwwe2lem9  8256  rpnnen1lem3  10340  rpnnen1lem5  10342  fseq1p1m1  10853  seqp1  11057  seqf1olem2  11082  seqf1o  11083  seqid  11087  seqz  11090  seqof  11099  bcval5  11326  bcn2  11327  hashf1lem1  11389  seqcoll  11397  s1fv  11442  swrdfv  11453  splfv1  11466  revfv  11477  shftcan1  11574  shftcan2  11575  climshft2  12052  isercoll2  12138  sumeq2w  12161  sumeq2ii  12162  cbvsum  12164  summo  12186  fsum  12189  fsumss  12194  fsumcvg2  12196  isumsplit  12295  rpnnen2lem1  12489  rpnnen2  12500  ruclem4  12508  sadfval  12639  smufval  12664  odzval  12852  1arithlem2  12967  vdwpc  13023  vdwlem6  13029  ramval  13051  setsid  13183  setsnid  13184  prdsval  13351  prdsplusgfval  13369  prdsmulrfval  13371  pwsvscaval  13390  imasval  13410  xpsc0  13458  xpsc1  13459  mrisval  13528  comfffval  13597  sectffval  13649  invinv  13668  oppcsect  13672  brssc  13687  issubc  13708  isfunc  13734  funcoppc  13745  idfuval  13746  idfu2  13748  idfu1  13750  idfucl  13751  cofuval  13752  cofu1  13754  cofu2  13756  cofuval2  13757  cofucl  13758  cofurid  13761  resfval  13762  resfval2  13763  funcres  13766  funcpropd  13770  isfull  13780  isnat  13817  fucco  13832  homafval  13857  idafval  13885  setcmon  13915  catcisolem  13934  catciso  13935  xpcval  13947  1stf1  13962  2ndf1  13965  1stfcl  13967  2ndfcl  13968  prfval  13969  prf2fval  13971  prf1st  13974  prf2nd  13975  1st2ndprf  13976  evlf2  13988  evlf2val  13989  evlfcl  13992  curfval  13993  curfpropd  14003  uncfval  14004  uncf2  14007  curfuncf  14008  diag11  14013  diag12  14014  diag2  14015  curf2ndf  14017  hofval  14022  hofcl  14029  yon11  14034  yon12  14035  yon2  14036  yonedalem4a  14045  yonedalem4b  14046  yonedalem4c  14047  yonedalem22  14048  yonedalem3b  14049  yonedainv  14051  yoniso  14055  lubval  14109  glbval  14114  joinfval  14117  meetfval  14124  isclat  14211  odumeet  14240  odujoin  14242  oduclatb  14244  poslubdg  14248  prdspjmhm  14439  pwsco1mhm  14442  gsumvalx  14447  gsumpropd  14449  gsumress  14450  gsumval2a  14455  grpsubfval  14520  grplactval  14559  grpsubpropd  14562  grpsubpropd2  14563  mulgfval  14564  mulgpropd  14596  submmulg  14598  pwsinvg  14603  subgmulg  14631  eqgfval  14661  lactghmga  14780  symgga  14782  cntrval  14791  cntzval  14793  cntzrcl  14799  oppgsubg  14832  ispgp  14899  vrgpval  15072  frgpup3lem  15082  frgpnabllem1  15157  frgpnabllem2  15158  gsumval3eu  15186  gsumval3  15187  gsumzres  15190  gsumzf1o  15192  gsumzaddlem  15199  gsumconst  15205  dmdprd  15232  dprdval  15234  dmdprdsplitlem  15268  dprd2da  15273  dpjfval  15286  dpjidcl  15289  dpjlid  15292  dpjrid  15293  dvrfval  15462  staffval  15608  srngnvl  15617  issrngd  15622  lspval  15728  islbs  15825  lbspropd  15848  lssacsex  15893  lbsacsbs  15905  sralem  15926  srasca  15930  sravsca  15931  rlmval  15941  lpival  15993  aspval  16064  psrmulval  16127  psrvscaval  16133  psrdi  16147  psrdir  16148  mvrval  16162  mvrval2  16163  mvrf1  16166  mplsubglem  16175  mplvscaval  16188  subrgmvrf  16202  opsrle  16213  opsrbaslem  16215  subrgasclcl  16236  psr1val  16261  vr1val  16267  coe1fv  16283  subrgvr1  16334  coe1addfv  16338  coe1subfv  16339  coe1tmfv1  16346  coe1tmfv2  16347  coe1tmmul2fv  16350  coe1pwmulfv  16352  coe1sclmulfv  16355  ply1sclid  16359  ply1sclf1  16360  zrhmulg  16460  chrval  16475  chrrhm  16481  znzrhval  16496  ocvval  16563  elocv  16564  cssval  16578  pjfval  16602  pjfo  16611  isobs  16616  ntrval  16769  clsval  16770  opncldf3  16819  neival  16835  lpfval  16866  lpval  16867  cnpval  16962  iscnp2  16965  isreg  17056  isnrm  17059  2ndcsep  17181  isnlly  17191  ptval  17261  dfac14  17308  cnmptk2  17376  pt1hmeo  17493  xkocnv  17501  fmval  17634  ufldom  17653  flimval  17654  flffval  17680  flfval  17681  cnpflf  17692  txflf  17697  fclsval  17699  fcfval  17724  symgtgp  17780  tgpconcomp  17791  prdstmdd  17802  txmetcnp  18089  subgnm2  18146  tngngp  18166  isnlm  18182  sranlm  18191  lssnlm  18207  nmofval  18219  nmoval  18220  isphtpy  18475  pcovalg  18506  pco1  18509  clmneg  18575  clmabs  18576  nmoleub2lem3  18592  nmoleub3  18596  cphcjcl  18615  cphnm  18625  cphipcj  18631  cphassr  18643  tchnmval  18656  tchcphlem3  18659  ipcau2  18660  tchcphlem1  18661  tchcphlem2  18662  tchcph  18663  ipcau  18664  ovolctb  18845  voliunlem3  18905  uniioombllem2  18934  vitalilem4  18962  mbflimsup  19017  itg1climres  19065  mbfi1fseqlem4  19069  mbfi1fseqlem5  19070  mbfi1fseqlem6  19071  mbfi1flimlem  19073  mbfmullem2  19075  mbfmullem  19076  itg2monolem1  19101  itg2mono  19104  itg2i1fseqle  19105  itg2i1fseq  19106  itg2addlem  19109  itg2cnlem1  19112  limcfval  19218  limcmpt2  19230  limcres  19232  cnplimc  19233  dvfval  19243  dvreslem  19255  dvres2lem  19256  dvn0  19269  dvnp1  19270  cpnfval  19277  elcpn  19279  dvaddbr  19283  dvmulbr  19284  dvcmul  19289  dvfre  19296  rolle  19333  cmvth  19334  mvth  19335  dvlip  19336  dvlipcn  19337  dvlip2  19338  c1liplem1  19339  dveq0  19343  dv11cn  19344  dvivthlem1  19351  dvivth  19353  dvne0  19354  lhop1lem  19356  lhop2  19358  lhop  19359  dvcnvrelem2  19361  dvcvx  19363  dvfsumabs  19366  ftc1lem6  19384  ftc2  19387  ftc2ditglem  19388  itgparts  19390  itgsubstlem  19391  evlslem1  19395  evlsval  19399  evlssca  19402  evlsvar  19403  evlval  19404  evl1sca  19409  evl1scad  19410  evl1var  19411  evl1vard  19412  evl1addd  19413  evl1subd  19414  evl1muld  19415  evl1vsd  19416  evl1expd  19417  pf1ind  19434  mdegaddle  19456  mdegmullem  19460  coe1mul3  19481  uc1pval  19521  mon1pval  19523  uc1pmon1p  19533  q1pval  19535  ply1remlem  19544  ply1rem  19545  fta1glem2  19548  fta1g  19549  fta1blem  19550  ig1pval  19554  plyeq0lem  19588  coeeulem  19602  coeid2  19617  dgrle  19621  dgreq  19622  0dgrb  19624  coemul  19629  coe11  19630  coe1term  19636  dgrlt  19643  dgradd2  19645  dgrcolem2  19651  plymul0or  19657  plydivlem4  19672  plydiveu  19674  plyremlem  19680  plyrem  19681  fta1  19684  vieta1lem2  19687  plyexmo  19689  aareccl  19702  aannenlem1  19704  aannenlem2  19705  taylfval  19734  tayl0  19737  dvtaylp  19745  dvntaylp0  19747  taylthlem1  19748  taylthlem2  19749  ulmval  19755  ulmres  19763  ulmshftlem  19764  ulmshft  19765  ulmcaulem  19767  ulmcau  19768  ulmss  19770  ulmdvlem1  19773  ulmdvlem3  19775  mtest  19777  mbfulm  19778  itgulm  19780  itgulm2  19781  pserval2  19783  pserulm  19794  psercn  19798  pserdvlem2  19800  pserdv  19801  pige3  19881  logtayl  20003  rlimcnp  20256  sqff1o  20416  muinv  20429  dchrinv  20496  sumdchr2  20505  dchr2sum  20508  lgsval4  20551  lgsmod  20556  lgsqrlem1  20576  dchrmusumlema  20638  dchrvmasumlem1  20640  dchrisum0re  20658  dchrisum0lema  20659  logsqvma2  20688  padicval  20762  grpoinvval  20886  grpodivfval  20903  gxfval  20918  gxval  20919  imsdval  21249  sspnval  21307  nmoofval  21334  nmooval  21335  bloval  21353  0oval  21360  nmlno0  21367  hmoval  21382  ajval  21434  ubth  21446  htthlem  21491  pjhval  21972  pjoc1  22009  pjoc2  22014  pjige0  22266  pjcjt2  22267  pjch  22269  pjsumi  22285  pjdsi  22287  pjds3i  22288  pjopyth  22295  pjnorm  22299  pjpyth  22300  pjnel  22301  hosval  22316  homval  22317  hodval  22318  hfsval  22319  hfmval  22320  braval  22520  kbval  22530  eigvalval  22536  leopg  22698  leoppos  22702  leoprf2  22703  leoprf  22704  elpjrn  22766  pj3cor1i  22785  strlem2  22827  hstrlem2  22835  ballotleme  23051  ballotlemi  23055  subfacp1lem5  23122  kur14  23154  ptpcon  23171  cvmliftmolem1  23219  cvmliftlem5  23227  cvmliftlem7  23229  cvmliftlem15  23236  cvmlift2lem3  23243  cvmlift2lem4  23244  cvmlift2lem7  23247  cvmlift2lem9  23249  cvmlift2  23254  cvmliftphtlem  23255  cvmlift3lem2  23258  cvmlift3lem5  23261  cvmlift3lem6  23262  cvmlift3lem7  23263  cvmlift3lem9  23265  cvmlift3  23266  iseupa  23288  vdgrfval  23296  vdgrval  23297  eupath2lem3  23310  eupath2  23311  relexp0  23432  relexpsucr  23433  brcgr  23938  bpolylem  24193  valpr  24569  repfuntw  24571  prjmapcp2  24581  valcurfn1  24615  valvalcurfn  24617  prodeq2  24718  dffprod  24730  fprodser  24731  islimrs  24991  valvze  25065  isucv  25088  mulmulvec  25098  distmlva  25099  distsava  25100  isder  25118  ishoma  25198  ishomd  25201  ismona  25220  isepia  25230  isiso  25236  cinvlem1  25239  isfuna  25245  isinob  25273  issrc  25278  propsrc  25279  isntr  25284  islimcat  25287  vtare  25296  vtarsu  25297  vtarl  25298  trclval  25305  isgraphmrph  25334  domcatfun  25336  domcatval  25341  codcatfun  25345  codcatval  25347  idmor  25357  cmp2morpdom  25375  isside0  25575  aishp  25583  isibcg  25602  neibastop3  25722  tailval  25733  filnetlem4  25741  cocanfo  25785  f1ocan2fv  25806  upixp  25814  sdclem2  25863  rrncmslem  25967  ismrer1  25973  isnacs  26190  mzpsubst  26237  eldioph2  26252  pw2f1ocnv  26541  fnwe2lem2  26559  dsmmval  26611  dsmm0cl  26617  prdsinvgd2  26619  frlmvscaval  26642  uvcval  26645  uvcvval  26646  uvcresum  26653  islnr3  26730  hbtlem1  26738  hbtlem2  26739  hbtlem7  26740  hbtlem4  26741  hbtlem5  26743  hbt  26745  dgrsub2  26750  dgrnznn  26751  mpaaeu  26766  mpaalem  26768  rgspnval  26784  flcidc  26790  pmtrval  26805  pmtrfv  26806  pmtrffv  26812  mdetfval  26898  cntzsdrg  26921  addrfv  27085  subrfv  27086  mulvfv  27087  refsum2cnlem1  27119  fmuldfeqlem1  27123  fmuldfeq  27124  fmul01lt1lem1  27125  fmul01lt1lem2  27126  stoweidlem17  27177  stoweidlem20  27180  stoweidlem27  27187  stoweidlem31  27191  stoweidlem34  27194  stoweidlem42  27202  stoweidlem44  27204  stoweidlem48  27208  stoweidlem59  27219  stirlinglem3  27236  stirlinglem15  27248  bnj1379  28142  lshpset  28447  lsatset  28459  lkrval  28557  eqlkr  28568  ldualvaddval  28600  ldualvsval  28607  ldualvsubval  28626  cmtfvalN  28679  isoml  28707  pmapval  29225  pclvalN  29358  polfvalN  29372  polvalN  29373  psubclsetN  29404  watfvalN  29460  watvalN  29461  ldilset  29577  ltrnfset  29585  ltrnset  29586  dilfsetN  29620  dilsetN  29621  trnfsetN  29623  trnsetN  29624  trlfset  29628  trlset  29629  trlval  29630  ltrnideq  29643  cdlemd8  29673  cdlemg1idlemN  30040  cdlemg1fvawlemN  30041  cdlemg2idN  30064  trlcoabs2N  30190  tgrpfset  30212  tgrpset  30213  tendofset  30226  tendoset  30227  erngfset  30267  erngset  30268  erngfset-rN  30275  erngset-rN  30276  cdlemi2  30287  cdlemj1  30289  cdlemk2  30300  cdlemk4  30302  cdlemk8  30306  cdlemkuu  30363  cdlemk31  30364  cdlemkuv2-3N  30367  cdlemk18-3N  30368  cdlemk22-3  30369  cdlemkfid2N  30391  cdlemkyu  30395  cdlemk19ylem  30398  cdlemk46  30416  cdlemk49  30419  cdlemk43N  30431  cdlemk19u1  30437  cdlemk19u  30438  dvafset  30472  dvaset  30473  dvaplusgv  30478  diaffval  30499  diafval  30500  diaval  30501  dvhfset  30549  dvhset  30550  dvhlveclem  30577  docaffvalN  30590  docafvalN  30591  docavalN  30592  djaffvalN  30602  djafvalN  30603  dibffval  30609  dibfval  30610  dibval  30611  dicffval  30643  dicfval  30644  dicval  30645  dicelvalN  30647  dicvaddcl  30659  dicvscacl  30660  cdlemn8  30673  cdlemn9  30674  dihordlem7b  30684  dihffval  30699  dihfval  30700  dihval  30701  dihopelvalcpre  30717  dihmeetlem1N  30759  dihglblem5apreN  30760  dihmeetlem4preN  30775  dihmeetlem13N  30788  dih1dimatlem0  30797  dochffval  30818  dochfval  30819  dochval  30820  djhffval  30865  djhfval  30866  lcfl7lem  30968  lclkrlem2k  30986  lclkrlem2u  30996  lcdfval  31057  lcdval  31058  lcdvaddval  31067  lcdvsval  31073  lcd0vvalN  31082  lcdvsubval  31087  lcdlsp  31090  mapdffval  31095  mapdfval  31096  mapdval  31097  hvmapffval  31227  hvmapfval  31228  hvmapval  31229  hvmapvalvalN  31230  hvmapidN  31231  hvmaplkr  31237  hdmap1ffval  31265  hdmap1fval  31266  hdmap1vallem  31267  hdmapffval  31298  hdmapfval  31299  hdmapval  31300  hdmapevec2  31308  hgmapffval  31357  hgmapfval  31358  hgmapval  31359  hdmaplna2  31382  hdmapglnm2  31383  hdmapinvlem3  31392  hlhilset  31406  hlhilipval  31421
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fv 5229
  Copyright terms: Public domain W3C validator