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

Theorem fveq1d 5693
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 5690 . 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 5417
This theorem is referenced by:  fveq12d  5697  csbfv2g  5703  funssfv  5709  fvmptd  5773  fvmpt2d  5777  mpteqb  5782  fvmptt  5783  fmptco  5864  fvunsn  5888  fvsng  5890  fsnunfv  5896  f1ocnvfv1  5977  f1ocnvfv2  5978  fcof1  5983  fcofo  5984  ofval  6277  offval2  6285  ofrfval2  6286  caofinvl  6294  curry1val  6402  curry2val  6406  fnwelem  6424  rdg0g  6648  oav  6718  omv  6719  oev  6721  resixpfo  7063  pw2f1olem  7175  mapxpen  7236  xpmapenlem  7237  ordtypelem6  7452  ordtypelem7  7453  unwdomg  7512  cantnffval  7578  cantnfval  7583  cantnfres  7593  cantnfp1lem3  7596  fseqenlem1  7865  fseqenlem2  7866  iunfictbso  7955  dfac12lem1  7983  dfac12lem2  7984  dfac12r  7986  ackbij2lem3  8081  ituni0  8258  itunisuc  8259  itunitc1  8260  ituniiun  8262  hsmexlem2  8267  hsmexlem4  8269  iundom2g  8375  konigthlem  8403  konigth  8404  fpwwe2lem6  8470  fpwwe2lem9  8473  rpnnen1lem3  10562  rpnnen1lem5  10564  fseq1p1m1  11081  seqp1  11297  seqf1olem2  11322  seqf1o  11323  seqid  11327  seqz  11330  seqof  11339  seqof2  11340  bcval5  11568  bcn2  11569  hashf1lem1  11663  seqcoll  11671  s1fv  11719  swrdfv  11730  splfv1  11743  revfv  11754  shftcan1  11857  shftcan2  11858  climshft2  12335  isercoll2  12421  sumeq2w  12445  sumeq2ii  12446  cbvsum  12448  summo  12470  fsum  12473  fsumss  12478  fsumcvg2  12480  isumsplit  12579  rpnnen2lem1  12773  rpnnen2  12784  ruclem4  12792  sadfval  12923  smufval  12948  odzval  13136  1arithlem2  13251  vdwpc  13307  vdwlem6  13313  ramval  13335  setsid  13467  setsnid  13468  prdsval  13637  prdsplusgfval  13655  prdsmulrfval  13657  pwsvscaval  13676  imasval  13696  xpsc0  13744  xpsc1  13745  mrisval  13814  comfffval  13883  sectffval  13935  invinv  13954  oppcsect  13958  brssc  13973  issubc  13994  isfunc  14020  funcoppc  14031  idfuval  14032  idfu2  14034  idfu1  14036  idfucl  14037  cofuval  14038  cofu1  14040  cofu2  14042  cofuval2  14043  cofucl  14044  cofurid  14047  resfval  14048  resfval2  14049  funcres  14052  funcpropd  14056  isfull  14066  isnat  14103  fucco  14118  homafval  14143  idafval  14171  setcmon  14201  catcisolem  14220  catciso  14221  xpcval  14233  1stf1  14248  2ndf1  14251  1stfcl  14253  2ndfcl  14254  prfval  14255  prf2fval  14257  prf1st  14260  prf2nd  14261  1st2ndprf  14262  evlf2  14274  evlf2val  14275  evlfcl  14278  curfval  14279  curfpropd  14289  uncfval  14290  uncf2  14293  curfuncf  14294  diag11  14299  diag12  14300  diag2  14301  curf2ndf  14303  hofval  14308  hofcl  14315  yon11  14320  yon12  14321  yon2  14322  yonedalem4a  14331  yonedalem4b  14332  yonedalem4c  14333  yonedalem22  14334  yonedalem3b  14335  yonedainv  14337  yoniso  14341  lubval  14395  glbval  14400  joinfval  14403  meetfval  14410  isclat  14497  odumeet  14526  odujoin  14528  oduclatb  14530  poslubdg  14534  prdspjmhm  14725  pwsco1mhm  14728  gsumvalx  14733  gsumpropd  14735  gsumress  14736  gsumval2a  14741  grpsubfval  14806  grplactval  14845  grpsubpropd  14848  grpsubpropd2  14849  mulgfval  14850  mulgpropd  14882  submmulg  14884  pwsinvg  14889  subgmulg  14917  eqgfval  14947  lactghmga  15066  symgga  15068  cntrval  15077  cntzval  15079  cntzrcl  15085  oppgsubg  15118  ispgp  15185  vrgpval  15358  frgpup3lem  15368  frgpnabllem1  15443  frgpnabllem2  15444  gsumval3eu  15472  gsumval3  15473  gsumzres  15476  gsumzf1o  15478  gsumzaddlem  15485  gsumconst  15491  dmdprd  15518  dprdval  15520  dmdprdsplitlem  15554  dprd2da  15559  dpjfval  15572  dpjidcl  15575  dpjlid  15578  dpjrid  15579  dvrfval  15748  staffval  15894  srngnvl  15903  issrngd  15908  lspval  16010  islbs  16107  lbspropd  16130  lssacsex  16175  lbsacsbs  16187  sralem  16208  srasca  16212  sravsca  16213  rlmval  16223  lpival  16275  aspval  16346  psrmulval  16409  psrvscaval  16415  psrdi  16429  psrdir  16430  mvrval  16444  mvrval2  16445  mvrf1  16448  mplsubglem  16457  mplvscaval  16470  subrgmvrf  16484  opsrle  16495  opsrbaslem  16497  subrgasclcl  16518  psr1val  16543  vr1val  16549  coe1fv  16563  subrgvr1  16613  coe1addfv  16617  coe1subfv  16618  coe1tmfv1  16625  coe1tmfv2  16626  coe1tmmul2fv  16629  coe1pwmulfv  16631  coe1sclmulfv  16634  ply1sclid  16638  ply1sclf1  16639  zrhmulg  16750  chrval  16765  chrrhm  16771  znzrhval  16786  ocvval  16853  elocv  16854  cssval  16868  pjfval  16892  pjfo  16901  isobs  16906  ntrval  17059  clsval  17060  opncldf3  17109  neival  17125  neiptopreu  17156  lpfval  17161  lpval  17162  cnpval  17258  iscnp2  17261  isreg  17354  isnrm  17357  2ndcsep  17479  isnlly  17489  ptval  17559  dfac14  17607  cnmptk2  17675  pt1hmeo  17795  xkocnv  17803  fmval  17932  ufldom  17951  flimval  17952  flffval  17978  flfval  17979  cnpflf  17990  txflf  17995  fclsval  17997  fcfval  18022  cnextval  18049  cnextfvval  18053  cnextcn  18055  cnextfres  18056  symgtgp  18088  tgpconcomp  18099  prdstmdd  18110  utopsnneiplem  18234  neipcfilu  18283  txmetcnp  18534  subgnm2  18632  tngngp  18652  isnlm  18668  sranlm  18677  lssnlm  18693  nmofval  18705  nmoval  18706  isphtpy  18963  pcovalg  18994  pco1  18997  clmneg  19063  clmabs  19064  nmoleub2lem3  19080  nmoleub3  19084  cphcjcl  19103  cphnm  19113  cphipcj  19119  cphassr  19131  tchnmval  19144  tchcphlem3  19147  ipcau2  19148  tchcphlem1  19149  tchcphlem2  19150  tchcph  19151  ipcau  19152  ovolctb  19343  voliunlem3  19403  uniioombllem2  19432  vitalilem4  19460  mbflimsup  19515  itg1climres  19563  mbfi1fseqlem4  19567  mbfi1fseqlem5  19568  mbfi1fseqlem6  19569  mbfi1flimlem  19571  mbfmullem2  19573  mbfmullem  19574  itg2monolem1  19599  itg2mono  19602  itg2i1fseqle  19603  itg2i1fseq  19604  itg2addlem  19607  itg2cnlem1  19610  limcfval  19716  limcmpt2  19728  limcres  19730  cnplimc  19731  dvfval  19741  dvreslem  19753  dvres2lem  19754  dvn0  19767  dvnp1  19768  cpnfval  19775  elcpn  19777  dvaddbr  19781  dvmulbr  19782  dvcmul  19787  dvfre  19794  rolle  19831  cmvth  19832  mvth  19833  dvlip  19834  dvlipcn  19835  dvlip2  19836  c1liplem1  19837  dveq0  19841  dv11cn  19842  dvivthlem1  19849  dvivth  19851  dvne0  19852  lhop1lem  19854  lhop2  19856  lhop  19857  dvcnvrelem2  19859  dvcvx  19861  dvfsumabs  19864  ftc1lem6  19882  ftc2  19885  ftc2ditglem  19886  itgparts  19888  itgsubstlem  19889  evlslem1  19893  evlsval  19897  evlssca  19900  evlsvar  19901  evlval  19902  evl1sca  19907  evl1scad  19908  evl1var  19909  evl1vard  19910  evl1addd  19911  evl1subd  19912  evl1muld  19913  evl1vsd  19914  evl1expd  19915  pf1ind  19932  mdegaddle  19954  mdegmullem  19958  coe1mul3  19979  uc1pval  20019  mon1pval  20021  uc1pmon1p  20031  q1pval  20033  ply1remlem  20042  ply1rem  20043  fta1glem2  20046  fta1g  20047  fta1blem  20048  ig1pval  20052  plyeq0lem  20086  coeeulem  20100  coeid2  20115  dgrle  20119  dgreq  20120  0dgrb  20122  coemul  20127  coe11  20128  coe1term  20134  dgrlt  20141  dgradd2  20143  dgrcolem2  20149  plymul0or  20155  plydivlem4  20170  plydiveu  20172  plyremlem  20178  plyrem  20179  fta1  20182  vieta1lem2  20185  plyexmo  20187  aareccl  20200  aannenlem1  20202  aannenlem2  20203  taylfval  20232  tayl0  20235  dvtaylp  20243  dvntaylp0  20245  taylthlem1  20246  taylthlem2  20247  ulmval  20253  ulmres  20261  ulmshftlem  20262  ulmshft  20263  ulmuni  20265  ulmcaulem  20267  ulmcau  20268  ulmss  20270  ulmdvlem1  20273  ulmdvlem3  20275  mtest  20277  mtestbdd  20278  mbfulm  20279  itgulm  20281  itgulm2  20282  pserval2  20284  pserulm  20295  psercn  20299  pserdvlem2  20301  pserdv  20302  pige3  20382  logtayl  20508  rlimcnp  20761  sqff1o  20922  muinv  20935  dchrinv  21002  sumdchr2  21011  dchr2sum  21014  lgsval4  21057  lgsmod  21062  lgsqrlem1  21082  dchrmusumlema  21144  dchrvmasumlem1  21146  dchrisum0re  21164  dchrisum0lema  21165  logsqvma2  21194  padicval  21268  vdgrfval  21623  vdgrval  21624  iseupa  21644  eupath2lem3  21658  eupath2  21659  grpoinvval  21770  grpodivfval  21787  gxfval  21802  gxval  21803  imsdval  22135  sspnval  22193  nmoofval  22220  nmooval  22221  bloval  22239  0oval  22246  nmlno0  22253  hmoval  22268  ajval  22320  ubth  22332  htthlem  22377  pjhval  22856  pjoc1  22893  pjoc2  22898  pjige0  23150  pjcjt2  23151  pjch  23153  pjsumi  23169  pjdsi  23171  pjds3i  23172  pjopyth  23179  pjnorm  23183  pjpyth  23184  pjnel  23185  hosval  23200  homval  23201  hodval  23202  hfsval  23203  hfmval  23204  braval  23404  kbval  23414  eigvalval  23420  leopg  23582  leoppos  23586  leoprf2  23587  leoprf  23588  elpjrn  23650  pj3cor1i  23669  strlem2  23711  hstrlem2  23719  fmptcof2  24033  offval2f  24037  fmcncfil  24274  nmmulg  24309  zrhnm  24310  qqhval  24315  qqhcn  24332  ofcfval  24438  ofcfval3  24442  brfae  24556  sitgval  24604  dstrvval  24685  ballotleme  24711  ballotlemi  24715  lgamgulmlem2  24771  lgamgulmlem5  24774  lgamgulm2  24777  lgamcvglem  24781  subfacp1lem5  24827  kur14  24859  ptpcon  24877  cvmliftmolem1  24925  cvmliftlem5  24933  cvmliftlem7  24935  cvmliftlem15  24942  cvmlift2lem3  24949  cvmlift2lem4  24950  cvmlift2lem7  24953  cvmlift2lem9  24955  cvmlift2  24960  cvmliftphtlem  24961  cvmlift3lem2  24964  cvmlift3lem5  24967  cvmlift3lem6  24968  cvmlift3lem7  24969  cvmlift3lem9  24971  cvmlift3  24972  relexp0  25086  relexpsucr  25087  shftvalg  25165  prodeq2w  25195  prodeq2ii  25196  prodmo  25219  fprod  25224  fprodss  25231  brcgr  25747  bpolylem  26002  neibastop3  26285  tailval  26296  filnetlem4  26304  cocanfo  26313  f1ocan2fv  26323  upixp  26325  sdclem2  26340  rrncmslem  26435  ismrer1  26441  isnacs  26652  mzpsubst  26699  eldioph2  26714  pw2f1ocnv  27002  fnwe2lem2  27020  dsmmval  27072  dsmm0cl  27078  prdsinvgd2  27080  frlmvscaval  27103  uvcval  27106  uvcvval  27107  uvcresum  27114  islnr3  27191  hbtlem1  27199  hbtlem2  27200  hbtlem7  27201  hbtlem4  27202  hbtlem5  27204  hbt  27206  dgrsub2  27211  dgrnznn  27212  mpaaeu  27227  mpaalem  27229  rgspnval  27245  flcidc  27251  pmtrval  27266  pmtrfv  27267  pmtrffv  27273  mdetfval  27359  cntzsdrg  27382  addrfv  27545  subrfv  27546  mulvfv  27547  refsum2cnlem1  27579  fmuldfeqlem1  27583  fmuldfeq  27584  fmul01lt1lem1  27585  fmul01lt1lem2  27586  stoweidlem17  27637  stoweidlem20  27640  stoweidlem27  27647  stoweidlem31  27651  stoweidlem34  27654  stoweidlem42  27662  stoweidlem44  27664  stoweidlem48  27668  stoweidlem59  27679  stirlinglem3  27696  stirlinglem15  27708  swrdswrd  28015  vdfrgra0  28130  vdgfrgra0  28131  bnj1379  28912  lshpset  29465  lsatset  29477  lkrval  29575  eqlkr  29586  ldualvaddval  29618  ldualvsval  29625  ldualvsubval  29644  cmtfvalN  29697  isoml  29725  pmapval  30243  pclvalN  30376  polfvalN  30390  polvalN  30391  psubclsetN  30422  watfvalN  30478  watvalN  30479  ldilset  30595  ltrnfset  30603  ltrnset  30604  dilfsetN  30638  dilsetN  30639  trnfsetN  30641  trnsetN  30642  trlfset  30646  trlset  30647  trlval  30648  ltrnideq  30661  cdlemd8  30691  cdlemg1idlemN  31058  cdlemg1fvawlemN  31059  cdlemg2idN  31082  trlcoabs2N  31208  tgrpfset  31230  tgrpset  31231  tendofset  31244  tendoset  31245  erngfset  31285  erngset  31286  erngfset-rN  31293  erngset-rN  31294  cdlemi2  31305  cdlemj1  31307  cdlemk2  31318  cdlemk4  31320  cdlemk8  31324  cdlemkuu  31381  cdlemk31  31382  cdlemkuv2-3N  31385  cdlemk18-3N  31386  cdlemk22-3  31387  cdlemkfid2N  31409  cdlemkyu  31413  cdlemk19ylem  31416  cdlemk46  31434  cdlemk49  31437  cdlemk43N  31449  cdlemk19u1  31455  cdlemk19u  31456  dvafset  31490  dvaset  31491  dvaplusgv  31496  diaffval  31517  diafval  31518  diaval  31519  dvhfset  31567  dvhset  31568  dvhlveclem  31595  docaffvalN  31608  docafvalN  31609  docavalN  31610  djaffvalN  31620  djafvalN  31621  dibffval  31627  dibfval  31628  dibval  31629  dicffval  31661  dicfval  31662  dicval  31663  dicelvalN  31665  dicvaddcl  31677  dicvscacl  31678  cdlemn8  31691  cdlemn9  31692  dihordlem7b  31702  dihffval  31717  dihfval  31718  dihval  31719  dihopelvalcpre  31735  dihmeetlem1N  31777  dihglblem5apreN  31778  dihmeetlem4preN  31793  dihmeetlem13N  31806  dih1dimatlem0  31815  dochffval  31836  dochfval  31837  dochval  31838  djhffval  31883  djhfval  31884  lcfl7lem  31986  lclkrlem2k  32004  lclkrlem2u  32014  lcdfval  32075  lcdval  32076  lcdvaddval  32085  lcdvsval  32091  lcd0vvalN  32100  lcdvsubval  32105  lcdlsp  32108  mapdffval  32113  mapdfval  32114  mapdval  32115  hvmapffval  32245  hvmapfval  32246  hvmapval  32247  hvmapvalvalN  32248  hvmapidN  32249  hvmaplkr  32255  hdmap1ffval  32283  hdmap1fval  32284  hdmap1vallem  32285  hdmapffval  32316  hdmapfval  32317  hdmapval  32318  hdmapevec2  32326  hgmapffval  32375  hgmapfval  32376  hgmapval  32377  hdmaplna2  32400  hdmapglnm2  32401  hdmapinvlem3  32410  hlhilset  32424  hlhilipval  32439
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425
  Copyright terms: Public domain W3C validator