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

Theorem fveq1d 5671
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 5668 . 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 1649   ` cfv 5395
This theorem is referenced by:  fveq12d  5675  csbfv2g  5681  funssfv  5687  fvmptd  5750  fvmpt2d  5754  mpteqb  5759  fvmptt  5760  fmptco  5841  fvunsn  5865  fvsng  5867  fsnunfv  5873  f1ocnvfv1  5954  f1ocnvfv2  5955  fcof1  5960  fcofo  5961  ofval  6254  offval2  6262  ofrfval2  6263  caofinvl  6271  curry1val  6379  curry2val  6383  fnwelem  6398  rdg0g  6622  oav  6692  omv  6693  oev  6695  resixpfo  7037  pw2f1olem  7149  mapxpen  7210  xpmapenlem  7211  ordtypelem6  7426  ordtypelem7  7427  unwdomg  7486  cantnffval  7552  cantnfval  7557  cantnfres  7567  cantnfp1lem3  7570  fseqenlem1  7839  fseqenlem2  7840  iunfictbso  7929  dfac12lem1  7957  dfac12lem2  7958  dfac12r  7960  ackbij2lem3  8055  ituni0  8232  itunisuc  8233  itunitc1  8234  ituniiun  8236  hsmexlem2  8241  hsmexlem4  8243  iundom2g  8349  konigthlem  8377  konigth  8378  fpwwe2lem6  8444  fpwwe2lem9  8447  rpnnen1lem3  10535  rpnnen1lem5  10537  fseq1p1m1  11053  seqp1  11266  seqf1olem2  11291  seqf1o  11292  seqid  11296  seqz  11299  seqof  11308  seqof2  11309  bcval5  11537  bcn2  11538  hashf1lem1  11632  seqcoll  11640  s1fv  11688  swrdfv  11699  splfv1  11712  revfv  11723  shftcan1  11826  shftcan2  11827  climshft2  12304  isercoll2  12390  sumeq2w  12414  sumeq2ii  12415  cbvsum  12417  summo  12439  fsum  12442  fsumss  12447  fsumcvg2  12449  isumsplit  12548  rpnnen2lem1  12742  rpnnen2  12753  ruclem4  12761  sadfval  12892  smufval  12917  odzval  13105  1arithlem2  13220  vdwpc  13276  vdwlem6  13282  ramval  13304  setsid  13436  setsnid  13437  prdsval  13606  prdsplusgfval  13624  prdsmulrfval  13626  pwsvscaval  13645  imasval  13665  xpsc0  13713  xpsc1  13714  mrisval  13783  comfffval  13852  sectffval  13904  invinv  13923  oppcsect  13927  brssc  13942  issubc  13963  isfunc  13989  funcoppc  14000  idfuval  14001  idfu2  14003  idfu1  14005  idfucl  14006  cofuval  14007  cofu1  14009  cofu2  14011  cofuval2  14012  cofucl  14013  cofurid  14016  resfval  14017  resfval2  14018  funcres  14021  funcpropd  14025  isfull  14035  isnat  14072  fucco  14087  homafval  14112  idafval  14140  setcmon  14170  catcisolem  14189  catciso  14190  xpcval  14202  1stf1  14217  2ndf1  14220  1stfcl  14222  2ndfcl  14223  prfval  14224  prf2fval  14226  prf1st  14229  prf2nd  14230  1st2ndprf  14231  evlf2  14243  evlf2val  14244  evlfcl  14247  curfval  14248  curfpropd  14258  uncfval  14259  uncf2  14262  curfuncf  14263  diag11  14268  diag12  14269  diag2  14270  curf2ndf  14272  hofval  14277  hofcl  14284  yon11  14289  yon12  14290  yon2  14291  yonedalem4a  14300  yonedalem4b  14301  yonedalem4c  14302  yonedalem22  14303  yonedalem3b  14304  yonedainv  14306  yoniso  14310  lubval  14364  glbval  14369  joinfval  14372  meetfval  14379  isclat  14466  odumeet  14495  odujoin  14497  oduclatb  14499  poslubdg  14503  prdspjmhm  14694  pwsco1mhm  14697  gsumvalx  14702  gsumpropd  14704  gsumress  14705  gsumval2a  14710  grpsubfval  14775  grplactval  14814  grpsubpropd  14817  grpsubpropd2  14818  mulgfval  14819  mulgpropd  14851  submmulg  14853  pwsinvg  14858  subgmulg  14886  eqgfval  14916  lactghmga  15035  symgga  15037  cntrval  15046  cntzval  15048  cntzrcl  15054  oppgsubg  15087  ispgp  15154  vrgpval  15327  frgpup3lem  15337  frgpnabllem1  15412  frgpnabllem2  15413  gsumval3eu  15441  gsumval3  15442  gsumzres  15445  gsumzf1o  15447  gsumzaddlem  15454  gsumconst  15460  dmdprd  15487  dprdval  15489  dmdprdsplitlem  15523  dprd2da  15528  dpjfval  15541  dpjidcl  15544  dpjlid  15547  dpjrid  15548  dvrfval  15717  staffval  15863  srngnvl  15872  issrngd  15877  lspval  15979  islbs  16076  lbspropd  16099  lssacsex  16144  lbsacsbs  16156  sralem  16177  srasca  16181  sravsca  16182  rlmval  16192  lpival  16244  aspval  16315  psrmulval  16378  psrvscaval  16384  psrdi  16398  psrdir  16399  mvrval  16413  mvrval2  16414  mvrf1  16417  mplsubglem  16426  mplvscaval  16439  subrgmvrf  16453  opsrle  16464  opsrbaslem  16466  subrgasclcl  16487  psr1val  16512  vr1val  16518  coe1fv  16532  subrgvr1  16582  coe1addfv  16586  coe1subfv  16587  coe1tmfv1  16594  coe1tmfv2  16595  coe1tmmul2fv  16598  coe1pwmulfv  16600  coe1sclmulfv  16603  ply1sclid  16607  ply1sclf1  16608  zrhmulg  16715  chrval  16730  chrrhm  16736  znzrhval  16751  ocvval  16818  elocv  16819  cssval  16833  pjfval  16857  pjfo  16866  isobs  16871  ntrval  17024  clsval  17025  opncldf3  17074  neival  17090  neiptopreu  17121  lpfval  17126  lpval  17127  cnpval  17223  iscnp2  17226  isreg  17319  isnrm  17322  2ndcsep  17444  isnlly  17454  ptval  17524  dfac14  17572  cnmptk2  17640  pt1hmeo  17760  xkocnv  17768  fmval  17897  ufldom  17916  flimval  17917  flffval  17943  flfval  17944  cnpflf  17955  txflf  17960  fclsval  17962  fcfval  17987  cnextval  18014  cnextfvval  18018  cnextcn  18020  cnextfres  18021  symgtgp  18053  tgpconcomp  18064  prdstmdd  18075  utopsnneiplem  18199  neipcfilu  18248  txmetcnp  18468  subgnm2  18547  tngngp  18567  isnlm  18583  sranlm  18592  lssnlm  18608  nmofval  18620  nmoval  18621  isphtpy  18878  pcovalg  18909  pco1  18912  clmneg  18978  clmabs  18979  nmoleub2lem3  18995  nmoleub3  18999  cphcjcl  19018  cphnm  19028  cphipcj  19034  cphassr  19046  tchnmval  19059  tchcphlem3  19062  ipcau2  19063  tchcphlem1  19064  tchcphlem2  19065  tchcph  19066  ipcau  19067  ovolctb  19254  voliunlem3  19314  uniioombllem2  19343  vitalilem4  19371  mbflimsup  19426  itg1climres  19474  mbfi1fseqlem4  19478  mbfi1fseqlem5  19479  mbfi1fseqlem6  19480  mbfi1flimlem  19482  mbfmullem2  19484  mbfmullem  19485  itg2monolem1  19510  itg2mono  19513  itg2i1fseqle  19514  itg2i1fseq  19515  itg2addlem  19518  itg2cnlem1  19521  limcfval  19627  limcmpt2  19639  limcres  19641  cnplimc  19642  dvfval  19652  dvreslem  19664  dvres2lem  19665  dvn0  19678  dvnp1  19679  cpnfval  19686  elcpn  19688  dvaddbr  19692  dvmulbr  19693  dvcmul  19698  dvfre  19705  rolle  19742  cmvth  19743  mvth  19744  dvlip  19745  dvlipcn  19746  dvlip2  19747  c1liplem1  19748  dveq0  19752  dv11cn  19753  dvivthlem1  19760  dvivth  19762  dvne0  19763  lhop1lem  19765  lhop2  19767  lhop  19768  dvcnvrelem2  19770  dvcvx  19772  dvfsumabs  19775  ftc1lem6  19793  ftc2  19796  ftc2ditglem  19797  itgparts  19799  itgsubstlem  19800  evlslem1  19804  evlsval  19808  evlssca  19811  evlsvar  19812  evlval  19813  evl1sca  19818  evl1scad  19819  evl1var  19820  evl1vard  19821  evl1addd  19822  evl1subd  19823  evl1muld  19824  evl1vsd  19825  evl1expd  19826  pf1ind  19843  mdegaddle  19865  mdegmullem  19869  coe1mul3  19890  uc1pval  19930  mon1pval  19932  uc1pmon1p  19942  q1pval  19944  ply1remlem  19953  ply1rem  19954  fta1glem2  19957  fta1g  19958  fta1blem  19959  ig1pval  19963  plyeq0lem  19997  coeeulem  20011  coeid2  20026  dgrle  20030  dgreq  20031  0dgrb  20033  coemul  20038  coe11  20039  coe1term  20045  dgrlt  20052  dgradd2  20054  dgrcolem2  20060  plymul0or  20066  plydivlem4  20081  plydiveu  20083  plyremlem  20089  plyrem  20090  fta1  20093  vieta1lem2  20096  plyexmo  20098  aareccl  20111  aannenlem1  20113  aannenlem2  20114  taylfval  20143  tayl0  20146  dvtaylp  20154  dvntaylp0  20156  taylthlem1  20157  taylthlem2  20158  ulmval  20164  ulmres  20172  ulmshftlem  20173  ulmshft  20174  ulmuni  20176  ulmcaulem  20178  ulmcau  20179  ulmss  20181  ulmdvlem1  20184  ulmdvlem3  20186  mtest  20188  mtestbdd  20189  mbfulm  20190  itgulm  20192  itgulm2  20193  pserval2  20195  pserulm  20206  psercn  20210  pserdvlem2  20212  pserdv  20213  pige3  20293  logtayl  20419  rlimcnp  20672  sqff1o  20833  muinv  20846  dchrinv  20913  sumdchr2  20922  dchr2sum  20925  lgsval4  20968  lgsmod  20973  lgsqrlem1  20993  dchrmusumlema  21055  dchrvmasumlem1  21057  dchrisum0re  21075  dchrisum0lema  21076  logsqvma2  21105  padicval  21179  vdgrfval  21515  vdgrval  21516  iseupa  21536  eupath2lem3  21550  eupath2  21551  grpoinvval  21662  grpodivfval  21679  gxfval  21694  gxval  21695  imsdval  22027  sspnval  22085  nmoofval  22112  nmooval  22113  bloval  22131  0oval  22138  nmlno0  22145  hmoval  22160  ajval  22212  ubth  22224  htthlem  22269  pjhval  22748  pjoc1  22785  pjoc2  22790  pjige0  23042  pjcjt2  23043  pjch  23045  pjsumi  23061  pjdsi  23063  pjds3i  23064  pjopyth  23071  pjnorm  23075  pjpyth  23076  pjnel  23077  hosval  23092  homval  23093  hodval  23094  hfsval  23095  hfmval  23096  braval  23296  kbval  23306  eigvalval  23312  leopg  23474  leoppos  23478  leoprf2  23479  leoprf  23480  elpjrn  23542  pj3cor1i  23561  strlem2  23603  hstrlem2  23611  fmptcof2  23919  offval2f  23923  fmcncfil  24122  nmmulg  24154  zrhnm  24155  qqhval  24158  qqhcn  24175  ofcfval  24278  ofcfval3  24282  brfae  24394  dstrvval  24508  ballotleme  24534  ballotlemi  24538  lgamgulmlem2  24594  lgamgulmlem5  24597  lgamgulm2  24600  lgamcvglem  24604  subfacp1lem5  24650  kur14  24682  ptpcon  24700  cvmliftmolem1  24748  cvmliftlem5  24756  cvmliftlem7  24758  cvmliftlem15  24765  cvmlift2lem3  24772  cvmlift2lem4  24773  cvmlift2lem7  24776  cvmlift2lem9  24778  cvmlift2  24783  cvmliftphtlem  24784  cvmlift3lem2  24787  cvmlift3lem5  24790  cvmlift3lem6  24791  cvmlift3lem7  24792  cvmlift3lem9  24794  cvmlift3  24795  relexp0  24909  relexpsucr  24910  shftvalg  24988  prodeq2w  25018  prodeq2ii  25019  prodmo  25042  fprod  25047  fprodss  25054  brcgr  25554  bpolylem  25809  itg2addnclem  25958  itg2addnc  25960  neibastop3  26083  tailval  26094  filnetlem4  26102  cocanfo  26111  f1ocan2fv  26121  upixp  26123  sdclem2  26138  rrncmslem  26233  ismrer1  26239  isnacs  26450  mzpsubst  26497  eldioph2  26512  pw2f1ocnv  26800  fnwe2lem2  26818  dsmmval  26870  dsmm0cl  26876  prdsinvgd2  26878  frlmvscaval  26901  uvcval  26904  uvcvval  26905  uvcresum  26912  islnr3  26989  hbtlem1  26997  hbtlem2  26998  hbtlem7  26999  hbtlem4  27000  hbtlem5  27002  hbt  27004  dgrsub2  27009  dgrnznn  27010  mpaaeu  27025  mpaalem  27027  rgspnval  27043  flcidc  27049  pmtrval  27064  pmtrfv  27065  pmtrffv  27071  mdetfval  27157  cntzsdrg  27180  addrfv  27343  subrfv  27344  mulvfv  27345  refsum2cnlem1  27377  fmuldfeqlem1  27381  fmuldfeq  27382  fmul01lt1lem1  27383  fmul01lt1lem2  27384  stoweidlem17  27435  stoweidlem20  27438  stoweidlem27  27445  stoweidlem31  27449  stoweidlem34  27452  stoweidlem42  27460  stoweidlem44  27462  stoweidlem48  27466  stoweidlem59  27477  stirlinglem3  27494  stirlinglem15  27506  vdfrgra0  27776  vdgfrgra0  27777  bnj1379  28541  lshpset  29094  lsatset  29106  lkrval  29204  eqlkr  29215  ldualvaddval  29247  ldualvsval  29254  ldualvsubval  29273  cmtfvalN  29326  isoml  29354  pmapval  29872  pclvalN  30005  polfvalN  30019  polvalN  30020  psubclsetN  30051  watfvalN  30107  watvalN  30108  ldilset  30224  ltrnfset  30232  ltrnset  30233  dilfsetN  30267  dilsetN  30268  trnfsetN  30270  trnsetN  30271  trlfset  30275  trlset  30276  trlval  30277  ltrnideq  30290  cdlemd8  30320  cdlemg1idlemN  30687  cdlemg1fvawlemN  30688  cdlemg2idN  30711  trlcoabs2N  30837  tgrpfset  30859  tgrpset  30860  tendofset  30873  tendoset  30874  erngfset  30914  erngset  30915  erngfset-rN  30922  erngset-rN  30923  cdlemi2  30934  cdlemj1  30936  cdlemk2  30947  cdlemk4  30949  cdlemk8  30953  cdlemkuu  31010  cdlemk31  31011  cdlemkuv2-3N  31014  cdlemk18-3N  31015  cdlemk22-3  31016  cdlemkfid2N  31038  cdlemkyu  31042  cdlemk19ylem  31045  cdlemk46  31063  cdlemk49  31066  cdlemk43N  31078  cdlemk19u1  31084  cdlemk19u  31085  dvafset  31119  dvaset  31120  dvaplusgv  31125  diaffval  31146  diafval  31147  diaval  31148  dvhfset  31196  dvhset  31197  dvhlveclem  31224  docaffvalN  31237  docafvalN  31238  docavalN  31239  djaffvalN  31249  djafvalN  31250  dibffval  31256  dibfval  31257  dibval  31258  dicffval  31290  dicfval  31291  dicval  31292  dicelvalN  31294  dicvaddcl  31306  dicvscacl  31307  cdlemn8  31320  cdlemn9  31321  dihordlem7b  31331  dihffval  31346  dihfval  31347  dihval  31348  dihopelvalcpre  31364  dihmeetlem1N  31406  dihglblem5apreN  31407  dihmeetlem4preN  31422  dihmeetlem13N  31435  dih1dimatlem0  31444  dochffval  31465  dochfval  31466  dochval  31467  djhffval  31512  djhfval  31513  lcfl7lem  31615  lclkrlem2k  31633  lclkrlem2u  31643  lcdfval  31704  lcdval  31705  lcdvaddval  31714  lcdvsval  31720  lcd0vvalN  31729  lcdvsubval  31734  lcdlsp  31737  mapdffval  31742  mapdfval  31743  mapdval  31744  hvmapffval  31874  hvmapfval  31875  hvmapval  31876  hvmapvalvalN  31877  hvmapidN  31878  hvmaplkr  31884  hdmap1ffval  31912  hdmap1fval  31913  hdmap1vallem  31914  hdmapffval  31945  hdmapfval  31946  hdmapval  31947  hdmapevec2  31955  hgmapffval  32004  hgmapfval  32005  hgmapval  32006  hdmaplna2  32029  hdmapglnm2  32030  hdmapinvlem3  32039  hlhilset  32053  hlhilipval  32068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403
  Copyright terms: Public domain W3C validator