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

Theorem fveq1d 5527
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 5524 . 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 5255
This theorem is referenced by:  fveq12d  5531  csbfv2g  5537  funssfv  5543  fvmptd  5606  mpteqb  5614  fvmptt  5615  fmptco  5691  fvunsn  5712  fvsng  5714  fsnunfv  5720  f1ocnvfv1  5792  f1ocnvfv2  5793  fcof1  5797  fcofo  5798  ofval  6087  offval2  6095  ofrfval2  6096  caofinvl  6104  curry1val  6211  curry2val  6215  fnwelem  6230  rdg0g  6440  oav  6510  omv  6511  oev  6513  resixpfo  6854  pw2f1olem  6966  mapxpen  7027  xpmapenlem  7028  ordtypelem6  7238  ordtypelem7  7239  unwdomg  7298  cantnffval  7364  cantnfval  7369  cantnfres  7379  cantnfp1lem3  7382  fseqenlem1  7651  fseqenlem2  7652  iunfictbso  7741  dfac12lem1  7769  dfac12lem2  7770  dfac12r  7772  ackbij2lem3  7867  ituni0  8044  itunisuc  8045  itunitc1  8046  ituniiun  8048  hsmexlem2  8053  hsmexlem4  8055  iundom2g  8162  konigthlem  8190  konigth  8191  fpwwe2lem6  8257  fpwwe2lem9  8260  rpnnen1lem3  10344  rpnnen1lem5  10346  fseq1p1m1  10857  seqp1  11061  seqf1olem2  11086  seqf1o  11087  seqid  11091  seqz  11094  seqof  11103  bcval5  11330  bcn2  11331  hashf1lem1  11393  seqcoll  11401  s1fv  11446  swrdfv  11457  splfv1  11470  revfv  11481  shftcan1  11578  shftcan2  11579  climshft2  12056  isercoll2  12142  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  summo  12190  fsum  12193  fsumss  12198  fsumcvg2  12200  isumsplit  12299  rpnnen2lem1  12493  rpnnen2  12504  ruclem4  12512  sadfval  12643  smufval  12668  odzval  12856  1arithlem2  12971  vdwpc  13027  vdwlem6  13033  ramval  13055  setsid  13187  setsnid  13188  prdsval  13355  prdsplusgfval  13373  prdsmulrfval  13375  pwsvscaval  13394  imasval  13414  xpsc0  13462  xpsc1  13463  mrisval  13532  comfffval  13601  sectffval  13653  invinv  13672  oppcsect  13676  brssc  13691  issubc  13712  isfunc  13738  funcoppc  13749  idfuval  13750  idfu2  13752  idfu1  13754  idfucl  13755  cofuval  13756  cofu1  13758  cofu2  13760  cofuval2  13761  cofucl  13762  cofurid  13765  resfval  13766  resfval2  13767  funcres  13770  funcpropd  13774  isfull  13784  isnat  13821  fucco  13836  homafval  13861  idafval  13889  setcmon  13919  catcisolem  13938  catciso  13939  xpcval  13951  1stf1  13966  2ndf1  13969  1stfcl  13971  2ndfcl  13972  prfval  13973  prf2fval  13975  prf1st  13978  prf2nd  13979  1st2ndprf  13980  evlf2  13992  evlf2val  13993  evlfcl  13996  curfval  13997  curfpropd  14007  uncfval  14008  uncf2  14011  curfuncf  14012  diag11  14017  diag12  14018  diag2  14019  curf2ndf  14021  hofval  14026  hofcl  14033  yon11  14038  yon12  14039  yon2  14040  yonedalem4a  14049  yonedalem4b  14050  yonedalem4c  14051  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  yoniso  14059  lubval  14113  glbval  14118  joinfval  14121  meetfval  14128  isclat  14215  odumeet  14244  odujoin  14246  oduclatb  14248  poslubdg  14252  prdspjmhm  14443  pwsco1mhm  14446  gsumvalx  14451  gsumpropd  14453  gsumress  14454  gsumval2a  14459  grpsubfval  14524  grplactval  14563  grpsubpropd  14566  grpsubpropd2  14567  mulgfval  14568  mulgpropd  14600  submmulg  14602  pwsinvg  14607  subgmulg  14635  eqgfval  14665  lactghmga  14784  symgga  14786  cntrval  14795  cntzval  14797  cntzrcl  14803  oppgsubg  14836  ispgp  14903  vrgpval  15076  frgpup3lem  15086  frgpnabllem1  15161  frgpnabllem2  15162  gsumval3eu  15190  gsumval3  15191  gsumzres  15194  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  dmdprd  15236  dprdval  15238  dmdprdsplitlem  15272  dprd2da  15277  dpjfval  15290  dpjidcl  15293  dpjlid  15296  dpjrid  15297  dvrfval  15466  staffval  15612  srngnvl  15621  issrngd  15626  lspval  15732  islbs  15829  lbspropd  15852  lssacsex  15897  lbsacsbs  15909  sralem  15930  srasca  15934  sravsca  15935  rlmval  15945  lpival  15997  aspval  16068  psrmulval  16131  psrvscaval  16137  psrdi  16151  psrdir  16152  mvrval  16166  mvrval2  16167  mvrf1  16170  mplsubglem  16179  mplvscaval  16192  subrgmvrf  16206  opsrle  16217  opsrbaslem  16219  subrgasclcl  16240  psr1val  16265  vr1val  16271  coe1fv  16287  subrgvr1  16338  coe1addfv  16342  coe1subfv  16343  coe1tmfv1  16350  coe1tmfv2  16351  coe1tmmul2fv  16354  coe1pwmulfv  16356  coe1sclmulfv  16359  ply1sclid  16363  ply1sclf1  16364  zrhmulg  16464  chrval  16479  chrrhm  16485  znzrhval  16500  ocvval  16567  elocv  16568  cssval  16582  pjfval  16606  pjfo  16615  isobs  16620  ntrval  16773  clsval  16774  opncldf3  16823  neival  16839  lpfval  16870  lpval  16871  cnpval  16966  iscnp2  16969  isreg  17060  isnrm  17063  2ndcsep  17185  isnlly  17195  ptval  17265  dfac14  17312  cnmptk2  17380  pt1hmeo  17497  xkocnv  17505  fmval  17638  ufldom  17657  flimval  17658  flffval  17684  flfval  17685  cnpflf  17696  txflf  17701  fclsval  17703  fcfval  17728  symgtgp  17784  tgpconcomp  17795  prdstmdd  17806  txmetcnp  18093  subgnm2  18150  tngngp  18170  isnlm  18186  sranlm  18195  lssnlm  18211  nmofval  18223  nmoval  18224  isphtpy  18479  pcovalg  18510  pco1  18513  clmneg  18579  clmabs  18580  nmoleub2lem3  18596  nmoleub3  18600  cphcjcl  18619  cphnm  18629  cphipcj  18635  cphassr  18647  tchnmval  18660  tchcphlem3  18663  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  tchcph  18667  ipcau  18668  ovolctb  18849  voliunlem3  18909  uniioombllem2  18938  vitalilem4  18966  mbflimsup  19021  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfmullem2  19079  mbfmullem  19080  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2cnlem1  19116  limcfval  19222  limcmpt2  19234  limcres  19236  cnplimc  19237  dvfval  19247  dvreslem  19259  dvres2lem  19260  dvn0  19273  dvnp1  19274  cpnfval  19281  elcpn  19283  dvaddbr  19287  dvmulbr  19288  dvcmul  19293  dvfre  19300  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dveq0  19347  dv11cn  19348  dvivthlem1  19355  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem2  19365  dvcvx  19367  dvfsumabs  19370  ftc1lem6  19388  ftc2  19391  ftc2ditglem  19392  itgparts  19394  itgsubstlem  19395  evlslem1  19399  evlsval  19403  evlssca  19406  evlsvar  19407  evlval  19408  evl1sca  19413  evl1scad  19414  evl1var  19415  evl1vard  19416  evl1addd  19417  evl1subd  19418  evl1muld  19419  evl1vsd  19420  evl1expd  19421  pf1ind  19438  mdegaddle  19460  mdegmullem  19464  coe1mul3  19485  uc1pval  19525  mon1pval  19527  uc1pmon1p  19537  q1pval  19539  ply1remlem  19548  ply1rem  19549  fta1glem2  19552  fta1g  19553  fta1blem  19554  ig1pval  19558  plyeq0lem  19592  coeeulem  19606  coeid2  19621  dgrle  19625  dgreq  19626  0dgrb  19628  coemul  19633  coe11  19634  coe1term  19640  dgrlt  19647  dgradd2  19649  dgrcolem2  19655  plymul0or  19661  plydivlem4  19676  plydiveu  19678  plyremlem  19684  plyrem  19685  fta1  19688  vieta1lem2  19691  plyexmo  19693  aareccl  19706  aannenlem1  19708  aannenlem2  19709  taylfval  19738  tayl0  19741  dvtaylp  19749  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmval  19759  ulmres  19767  ulmshftlem  19768  ulmshft  19769  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  mbfulm  19782  itgulm  19784  itgulm2  19785  pserval2  19787  pserulm  19798  psercn  19802  pserdvlem2  19804  pserdv  19805  pige3  19885  logtayl  20007  rlimcnp  20260  sqff1o  20420  muinv  20433  dchrinv  20500  sumdchr2  20509  dchr2sum  20512  lgsval4  20555  lgsmod  20560  lgsqrlem1  20580  dchrmusumlema  20642  dchrvmasumlem1  20644  dchrisum0re  20662  dchrisum0lema  20663  logsqvma2  20692  padicval  20766  grpoinvval  20892  grpodivfval  20909  gxfval  20924  gxval  20925  imsdval  21255  sspnval  21313  nmoofval  21340  nmooval  21341  bloval  21359  0oval  21366  nmlno0  21373  hmoval  21388  ajval  21440  ubth  21452  htthlem  21497  pjhval  21976  pjoc1  22013  pjoc2  22018  pjige0  22270  pjcjt2  22271  pjch  22273  pjsumi  22289  pjdsi  22291  pjds3i  22292  pjopyth  22299  pjnorm  22303  pjpyth  22304  pjnel  22305  hosval  22320  homval  22321  hodval  22322  hfsval  22323  hfmval  22324  braval  22524  kbval  22534  eigvalval  22540  leopg  22702  leoppos  22706  leoprf2  22707  leoprf  22708  elpjrn  22770  pj3cor1i  22789  strlem2  22831  hstrlem2  22839  ballotleme  23055  ballotlemi  23059  fvmpt2d  23225  fmptcof2  23229  offval2f  23233  ofcfval  23459  ofcfval3  23463  itgmeq123dTMP  23589  dstrvval  23671  subfacp1lem5  23715  kur14  23747  ptpcon  23764  cvmliftmolem1  23812  cvmliftlem5  23820  cvmliftlem7  23822  cvmliftlem15  23829  cvmlift2lem3  23836  cvmlift2lem4  23837  cvmlift2lem7  23840  cvmlift2lem9  23842  cvmlift2  23847  cvmliftphtlem  23848  cvmlift3lem2  23851  cvmlift3lem5  23854  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  iseupa  23881  vdgrfval  23889  vdgrval  23890  eupath2lem3  23903  eupath2  23904  relexp0  24025  relexpsucr  24026  brcgr  24528  bpolylem  24783  valpr  25158  prjmapcp2  25170  valcurfn1  25204  valvalcurfn  25206  prodeq2  25307  dffprod  25319  fprodser  25320  islimrs  25580  valvze  25654  isucv  25677  mulmulvec  25687  distmlva  25688  distsava  25689  isder  25707  ishoma  25787  ishomd  25790  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  isfuna  25834  isinob  25862  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  vtare  25885  vtarsu  25886  vtarl  25887  trclval  25894  isgraphmrph  25923  domcatfun  25925  domcatval  25930  codcatfun  25934  codcatval  25936  idmor  25946  cmp2morpdom  25964  isside0  26164  aishp  26172  isibcg  26191  neibastop3  26311  tailval  26322  filnetlem4  26330  cocanfo  26374  f1ocan2fv  26395  upixp  26403  sdclem2  26452  rrncmslem  26556  ismrer1  26562  isnacs  26779  mzpsubst  26826  eldioph2  26841  pw2f1ocnv  27130  fnwe2lem2  27148  dsmmval  27200  dsmm0cl  27206  prdsinvgd2  27208  frlmvscaval  27231  uvcval  27234  uvcvval  27235  uvcresum  27242  islnr3  27319  hbtlem1  27327  hbtlem2  27328  hbtlem7  27329  hbtlem4  27330  hbtlem5  27332  hbt  27334  dgrsub2  27339  dgrnznn  27340  mpaaeu  27355  mpaalem  27357  rgspnval  27373  flcidc  27379  pmtrval  27394  pmtrfv  27395  pmtrffv  27401  mdetfval  27487  cntzsdrg  27510  addrfv  27674  subrfv  27675  mulvfv  27676  refsum2cnlem1  27708  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  stoweidlem17  27766  stoweidlem20  27769  stoweidlem27  27776  stoweidlem31  27780  stoweidlem34  27783  stoweidlem42  27791  stoweidlem44  27793  stoweidlem48  27797  stoweidlem59  27808  stirlinglem3  27825  stirlinglem15  27837  bnj1379  28863  lshpset  29168  lsatset  29180  lkrval  29278  eqlkr  29289  ldualvaddval  29321  ldualvsval  29328  ldualvsubval  29347  cmtfvalN  29400  isoml  29428  pmapval  29946  pclvalN  30079  polfvalN  30093  polvalN  30094  psubclsetN  30125  watfvalN  30181  watvalN  30182  ldilset  30298  ltrnfset  30306  ltrnset  30307  dilfsetN  30341  dilsetN  30342  trnfsetN  30344  trnsetN  30345  trlfset  30349  trlset  30350  trlval  30351  ltrnideq  30364  cdlemd8  30394  cdlemg1idlemN  30761  cdlemg1fvawlemN  30762  cdlemg2idN  30785  trlcoabs2N  30911  tgrpfset  30933  tgrpset  30934  tendofset  30947  tendoset  30948  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  cdlemi2  31008  cdlemj1  31010  cdlemk2  31021  cdlemk4  31023  cdlemk8  31027  cdlemkuu  31084  cdlemk31  31085  cdlemkuv2-3N  31088  cdlemk18-3N  31089  cdlemk22-3  31090  cdlemkfid2N  31112  cdlemkyu  31116  cdlemk19ylem  31119  cdlemk46  31137  cdlemk49  31140  cdlemk43N  31152  cdlemk19u1  31158  cdlemk19u  31159  dvafset  31193  dvaset  31194  dvaplusgv  31199  diaffval  31220  diafval  31221  diaval  31222  dvhfset  31270  dvhset  31271  dvhlveclem  31298  docaffvalN  31311  docafvalN  31312  docavalN  31313  djaffvalN  31323  djafvalN  31324  dibffval  31330  dibfval  31331  dibval  31332  dicffval  31364  dicfval  31365  dicval  31366  dicelvalN  31368  dicvaddcl  31380  dicvscacl  31381  cdlemn8  31394  cdlemn9  31395  dihordlem7b  31405  dihffval  31420  dihfval  31421  dihval  31422  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem4preN  31496  dihmeetlem13N  31509  dih1dimatlem0  31518  dochffval  31539  dochfval  31540  dochval  31541  djhffval  31586  djhfval  31587  lcfl7lem  31689  lclkrlem2k  31707  lclkrlem2u  31717  lcdfval  31778  lcdval  31779  lcdvaddval  31788  lcdvsval  31794  lcd0vvalN  31803  lcdvsubval  31808  lcdlsp  31811  mapdffval  31816  mapdfval  31817  mapdval  31818  hvmapffval  31948  hvmapfval  31949  hvmapval  31950  hvmapvalvalN  31951  hvmapidN  31952  hvmaplkr  31958  hdmap1ffval  31986  hdmap1fval  31987  hdmap1vallem  31988  hdmapffval  32019  hdmapfval  32020  hdmapval  32021  hdmapevec2  32029  hgmapffval  32078  hgmapfval  32079  hgmapval  32080  hdmaplna2  32103  hdmapglnm2  32104  hdmapinvlem3  32113  hlhilset  32127  hlhilipval  32142
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator