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

Theorem fveq1d 5721
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 5718 . 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 5445
This theorem is referenced by:  fveq12d  5725  csbfv2g  5731  funssfv  5737  fvmptd  5801  fvmpt2d  5805  mpteqb  5810  fvmptt  5811  fmptco  5892  fvunsn  5916  fvsng  5918  fsnunfv  5924  f1ocnvfv1  6005  f1ocnvfv2  6006  fcof1  6011  fcofo  6012  ofval  6305  offval2  6313  ofrfval2  6314  caofinvl  6322  curry1val  6430  curry2val  6434  fnwelem  6452  rdg0g  6676  oav  6746  omv  6747  oev  6749  resixpfo  7091  pw2f1olem  7203  mapxpen  7264  xpmapenlem  7265  ordtypelem6  7481  ordtypelem7  7482  unwdomg  7541  cantnffval  7607  cantnfval  7612  cantnfres  7622  cantnfp1lem3  7625  fseqenlem1  7894  fseqenlem2  7895  iunfictbso  7984  dfac12lem1  8012  dfac12lem2  8013  dfac12r  8015  ackbij2lem3  8110  ituni0  8287  itunisuc  8288  itunitc1  8289  ituniiun  8291  hsmexlem2  8296  hsmexlem4  8298  iundom2g  8404  konigthlem  8432  konigth  8433  fpwwe2lem6  8499  fpwwe2lem9  8502  rpnnen1lem3  10591  rpnnen1lem5  10593  fseq1p1m1  11110  seqp1  11326  seqf1olem2  11351  seqf1o  11352  seqid  11356  seqz  11359  seqof  11368  seqof2  11369  bcval5  11597  bcn2  11598  hashf1lem1  11692  seqcoll  11700  s1fv  11748  swrdfv  11759  splfv1  11772  revfv  11783  shftcan1  11886  shftcan2  11887  climshft2  12364  isercoll2  12450  sumeq2w  12474  sumeq2ii  12475  cbvsum  12477  summo  12499  fsum  12502  fsumss  12507  fsumcvg2  12509  isumsplit  12608  rpnnen2lem1  12802  rpnnen2  12813  ruclem4  12821  sadfval  12952  smufval  12977  odzval  13165  1arithlem2  13280  vdwpc  13336  vdwlem6  13342  ramval  13364  setsid  13496  setsnid  13497  prdsval  13666  prdsplusgfval  13684  prdsmulrfval  13686  pwsvscaval  13705  imasval  13725  xpsc0  13773  xpsc1  13774  mrisval  13843  comfffval  13912  sectffval  13964  invinv  13983  oppcsect  13987  brssc  14002  issubc  14023  isfunc  14049  funcoppc  14060  idfuval  14061  idfu2  14063  idfu1  14065  idfucl  14066  cofuval  14067  cofu1  14069  cofu2  14071  cofuval2  14072  cofucl  14073  cofurid  14076  resfval  14077  resfval2  14078  funcres  14081  funcpropd  14085  isfull  14095  isnat  14132  fucco  14147  homafval  14172  idafval  14200  setcmon  14230  catcisolem  14249  catciso  14250  xpcval  14262  1stf1  14277  2ndf1  14280  1stfcl  14282  2ndfcl  14283  prfval  14284  prf2fval  14286  prf1st  14289  prf2nd  14290  1st2ndprf  14291  evlf2  14303  evlf2val  14304  evlfcl  14307  curfval  14308  curfpropd  14318  uncfval  14319  uncf2  14322  curfuncf  14323  diag11  14328  diag12  14329  diag2  14330  curf2ndf  14332  hofval  14337  hofcl  14344  yon11  14349  yon12  14350  yon2  14351  yonedalem4a  14360  yonedalem4b  14361  yonedalem4c  14362  yonedalem22  14363  yonedalem3b  14364  yonedainv  14366  yoniso  14370  lubval  14424  glbval  14429  joinfval  14432  meetfval  14439  isclat  14526  odumeet  14555  odujoin  14557  oduclatb  14559  poslubdg  14563  prdspjmhm  14754  pwsco1mhm  14757  gsumvalx  14762  gsumpropd  14764  gsumress  14765  gsumval2a  14770  grpsubfval  14835  grplactval  14874  grpsubpropd  14877  grpsubpropd2  14878  mulgfval  14879  mulgpropd  14911  submmulg  14913  pwsinvg  14918  subgmulg  14946  eqgfval  14976  lactghmga  15095  symgga  15097  cntrval  15106  cntzval  15108  cntzrcl  15114  oppgsubg  15147  ispgp  15214  vrgpval  15387  frgpup3lem  15397  frgpnabllem1  15472  frgpnabllem2  15473  gsumval3eu  15501  gsumval3  15502  gsumzres  15505  gsumzf1o  15507  gsumzaddlem  15514  gsumconst  15520  dmdprd  15547  dprdval  15549  dmdprdsplitlem  15583  dprd2da  15588  dpjfval  15601  dpjidcl  15604  dpjlid  15607  dpjrid  15608  dvrfval  15777  staffval  15923  srngnvl  15932  issrngd  15937  lspval  16039  islbs  16136  lbspropd  16159  lssacsex  16204  lbsacsbs  16216  sralem  16237  srasca  16241  sravsca  16242  rlmval  16252  lpival  16304  aspval  16375  psrmulval  16438  psrvscaval  16444  psrdi  16458  psrdir  16459  mvrval  16473  mvrval2  16474  mvrf1  16477  mplsubglem  16486  mplvscaval  16499  subrgmvrf  16513  opsrle  16524  opsrbaslem  16526  subrgasclcl  16547  psr1val  16572  vr1val  16578  coe1fv  16592  subrgvr1  16642  coe1addfv  16646  coe1subfv  16647  coe1tmfv1  16654  coe1tmfv2  16655  coe1tmmul2fv  16658  coe1pwmulfv  16660  coe1sclmulfv  16663  ply1sclid  16667  ply1sclf1  16668  zrhmulg  16779  chrval  16794  chrrhm  16800  znzrhval  16815  ocvval  16882  elocv  16883  cssval  16897  pjfval  16921  pjfo  16930  isobs  16935  ntrval  17088  clsval  17089  opncldf3  17138  neival  17154  neiptopreu  17185  lpfval  17190  lpval  17191  cnpval  17288  iscnp2  17291  isreg  17384  isnrm  17387  2ndcsep  17510  isnlly  17520  ptval  17590  dfac14  17638  cnmptk2  17706  pt1hmeo  17826  xkocnv  17834  fmval  17963  ufldom  17982  flimval  17983  flffval  18009  flfval  18010  cnpflf  18021  txflf  18026  fclsval  18028  fcfval  18053  cnextval  18080  cnextfvval  18084  cnextcn  18086  cnextfres  18087  symgtgp  18119  tgpconcomp  18130  prdstmdd  18141  utopsnneiplem  18265  neipcfilu  18314  txmetcnp  18565  subgnm2  18663  tngngp  18683  isnlm  18699  sranlm  18708  lssnlm  18724  nmofval  18736  nmoval  18737  isphtpy  18994  pcovalg  19025  pco1  19028  clmneg  19094  clmabs  19095  nmoleub2lem3  19111  nmoleub3  19115  cphcjcl  19134  cphnm  19144  cphipcj  19150  cphassr  19162  tchnmval  19175  tchcphlem3  19178  ipcau2  19179  tchcphlem1  19180  tchcphlem2  19181  tchcph  19182  ipcau  19183  ovolctb  19374  voliunlem3  19434  uniioombllem2  19463  vitalilem4  19491  mbflimsup  19546  itg1climres  19594  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1fseqlem6  19600  mbfi1flimlem  19602  mbfmullem2  19604  mbfmullem  19605  itg2monolem1  19630  itg2mono  19633  itg2i1fseqle  19634  itg2i1fseq  19635  itg2addlem  19638  itg2cnlem1  19641  limcfval  19747  limcmpt2  19759  limcres  19761  cnplimc  19762  dvfval  19772  dvreslem  19784  dvres2lem  19785  dvn0  19798  dvnp1  19799  cpnfval  19806  elcpn  19808  dvaddbr  19812  dvmulbr  19813  dvcmul  19818  dvfre  19825  rolle  19862  cmvth  19863  mvth  19864  dvlip  19865  dvlipcn  19866  dvlip2  19867  c1liplem1  19868  dveq0  19872  dv11cn  19873  dvivthlem1  19880  dvivth  19882  dvne0  19883  lhop1lem  19885  lhop2  19887  lhop  19888  dvcnvrelem2  19890  dvcvx  19892  dvfsumabs  19895  ftc1lem6  19913  ftc2  19916  ftc2ditglem  19917  itgparts  19919  itgsubstlem  19920  evlslem1  19924  evlsval  19928  evlssca  19931  evlsvar  19932  evlval  19933  evl1sca  19938  evl1scad  19939  evl1var  19940  evl1vard  19941  evl1addd  19942  evl1subd  19943  evl1muld  19944  evl1vsd  19945  evl1expd  19946  pf1ind  19963  mdegaddle  19985  mdegmullem  19989  coe1mul3  20010  uc1pval  20050  mon1pval  20052  uc1pmon1p  20062  q1pval  20064  ply1remlem  20073  ply1rem  20074  fta1glem2  20077  fta1g  20078  fta1blem  20079  ig1pval  20083  plyeq0lem  20117  coeeulem  20131  coeid2  20146  dgrle  20150  dgreq  20151  0dgrb  20153  coemul  20158  coe11  20159  coe1term  20165  dgrlt  20172  dgradd2  20174  dgrcolem2  20180  plymul0or  20186  plydivlem4  20201  plydiveu  20203  plyremlem  20209  plyrem  20210  fta1  20213  vieta1lem2  20216  plyexmo  20218  aareccl  20231  aannenlem1  20233  aannenlem2  20234  taylfval  20263  tayl0  20266  dvtaylp  20274  dvntaylp0  20276  taylthlem1  20277  taylthlem2  20278  ulmval  20284  ulmres  20292  ulmshftlem  20293  ulmshft  20294  ulmuni  20296  ulmcaulem  20298  ulmcau  20299  ulmss  20301  ulmdvlem1  20304  ulmdvlem3  20306  mtest  20308  mtestbdd  20309  mbfulm  20310  itgulm  20312  itgulm2  20313  pserval2  20315  pserulm  20326  psercn  20330  pserdvlem2  20332  pserdv  20333  pige3  20413  logtayl  20539  rlimcnp  20792  sqff1o  20953  muinv  20966  dchrinv  21033  sumdchr2  21042  dchr2sum  21045  lgsval4  21088  lgsmod  21093  lgsqrlem1  21113  dchrmusumlema  21175  dchrvmasumlem1  21177  dchrisum0re  21195  dchrisum0lema  21196  logsqvma2  21225  padicval  21299  vdgrfval  21654  vdgrval  21655  iseupa  21675  eupath2lem3  21689  eupath2  21690  grpoinvval  21801  grpodivfval  21818  gxfval  21833  gxval  21834  imsdval  22166  sspnval  22224  nmoofval  22251  nmooval  22252  bloval  22270  0oval  22277  nmlno0  22284  hmoval  22299  ajval  22351  ubth  22363  htthlem  22408  pjhval  22887  pjoc1  22924  pjoc2  22929  pjige0  23181  pjcjt2  23182  pjch  23184  pjsumi  23200  pjdsi  23202  pjds3i  23203  pjopyth  23210  pjnorm  23214  pjpyth  23215  pjnel  23216  hosval  23231  homval  23232  hodval  23233  hfsval  23234  hfmval  23235  braval  23435  kbval  23445  eigvalval  23451  leopg  23613  leoppos  23617  leoprf2  23618  leoprf  23619  elpjrn  23681  pj3cor1i  23700  strlem2  23742  hstrlem2  23750  fmptcof2  24064  offval2f  24068  fmcncfil  24305  nmmulg  24340  zrhnm  24341  qqhval  24346  qqhcn  24363  ofcfval  24469  ofcfval3  24473  brfae  24587  sitgval  24635  dstrvval  24716  ballotleme  24742  ballotlemi  24746  lgamgulmlem2  24802  lgamgulmlem5  24805  lgamgulm2  24808  lgamcvglem  24812  subfacp1lem5  24858  kur14  24890  ptpcon  24908  cvmliftmolem1  24956  cvmliftlem5  24964  cvmliftlem7  24966  cvmliftlem15  24973  cvmlift2lem3  24980  cvmlift2lem4  24981  cvmlift2lem7  24984  cvmlift2lem9  24986  cvmlift2  24991  cvmliftphtlem  24992  cvmlift3lem2  24995  cvmlift3lem5  24998  cvmlift3lem6  24999  cvmlift3lem7  25000  cvmlift3lem9  25002  cvmlift3  25003  relexp0  25117  relexpsucr  25118  shftvalg  25196  prodeq2w  25227  prodeq2ii  25228  prodmo  25251  fprod  25256  fprodss  25263  brcgr  25787  bpolylem  26042  neibastop3  26328  tailval  26339  filnetlem4  26347  cocanfo  26356  f1ocan2fv  26366  upixp  26368  sdclem2  26383  rrncmslem  26478  ismrer1  26484  isnacs  26695  mzpsubst  26742  eldioph2  26757  pw2f1ocnv  27045  fnwe2lem2  27063  dsmmval  27115  dsmm0cl  27121  prdsinvgd2  27123  frlmvscaval  27146  uvcval  27149  uvcvval  27150  uvcresum  27157  islnr3  27234  hbtlem1  27242  hbtlem2  27243  hbtlem7  27244  hbtlem4  27245  hbtlem5  27247  hbt  27249  dgrsub2  27254  dgrnznn  27255  mpaaeu  27270  mpaalem  27272  rgspnval  27288  flcidc  27294  pmtrval  27309  pmtrfv  27310  pmtrffv  27316  mdetfval  27402  cntzsdrg  27425  addrfv  27588  subrfv  27589  mulvfv  27590  refsum2cnlem1  27622  fmuldfeqlem1  27626  fmuldfeq  27627  fmul01lt1lem1  27628  fmul01lt1lem2  27629  stoweidlem17  27680  stoweidlem20  27683  stoweidlem27  27690  stoweidlem31  27694  stoweidlem34  27697  stoweidlem42  27705  stoweidlem44  27707  stoweidlem48  27711  stoweidlem59  27722  stirlinglem3  27739  stirlinglem15  27751  swrdswrd  28086  isshwrd  28121  shwrdidx  28130  shwrdidx0  28132  2shwrdid  28147  2shwrdcom  28153  shwrdeqdif2  28156  shwrdssizelem2  28167  shwrdssizesame  28171  shwrdsdisj  28173  vdfrgra0  28270  vdgfrgra0  28271  bnj1379  29056  lshpset  29615  lsatset  29627  lkrval  29725  eqlkr  29736  ldualvaddval  29768  ldualvsval  29775  ldualvsubval  29794  cmtfvalN  29847  isoml  29875  pmapval  30393  pclvalN  30526  polfvalN  30540  polvalN  30541  psubclsetN  30572  watfvalN  30628  watvalN  30629  ldilset  30745  ltrnfset  30753  ltrnset  30754  dilfsetN  30788  dilsetN  30789  trnfsetN  30791  trnsetN  30792  trlfset  30796  trlset  30797  trlval  30798  ltrnideq  30811  cdlemd8  30841  cdlemg1idlemN  31208  cdlemg1fvawlemN  31209  cdlemg2idN  31232  trlcoabs2N  31358  tgrpfset  31380  tgrpset  31381  tendofset  31394  tendoset  31395  erngfset  31435  erngset  31436  erngfset-rN  31443  erngset-rN  31444  cdlemi2  31455  cdlemj1  31457  cdlemk2  31468  cdlemk4  31470  cdlemk8  31474  cdlemkuu  31531  cdlemk31  31532  cdlemkuv2-3N  31535  cdlemk18-3N  31536  cdlemk22-3  31537  cdlemkfid2N  31559  cdlemkyu  31563  cdlemk19ylem  31566  cdlemk46  31584  cdlemk49  31587  cdlemk43N  31599  cdlemk19u1  31605  cdlemk19u  31606  dvafset  31640  dvaset  31641  dvaplusgv  31646  diaffval  31667  diafval  31668  diaval  31669  dvhfset  31717  dvhset  31718  dvhlveclem  31745  docaffvalN  31758  docafvalN  31759  docavalN  31760  djaffvalN  31770  djafvalN  31771  dibffval  31777  dibfval  31778  dibval  31779  dicffval  31811  dicfval  31812  dicval  31813  dicelvalN  31815  dicvaddcl  31827  dicvscacl  31828  cdlemn8  31841  cdlemn9  31842  dihordlem7b  31852  dihffval  31867  dihfval  31868  dihval  31869  dihopelvalcpre  31885  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem4preN  31943  dihmeetlem13N  31956  dih1dimatlem0  31965  dochffval  31986  dochfval  31987  dochval  31988  djhffval  32033  djhfval  32034  lcfl7lem  32136  lclkrlem2k  32154  lclkrlem2u  32164  lcdfval  32225  lcdval  32226  lcdvaddval  32235  lcdvsval  32241  lcd0vvalN  32250  lcdvsubval  32255  lcdlsp  32258  mapdffval  32263  mapdfval  32264  mapdval  32265  hvmapffval  32395  hvmapfval  32396  hvmapval  32397  hvmapvalvalN  32398  hvmapidN  32399  hvmaplkr  32405  hdmap1ffval  32433  hdmap1fval  32434  hdmap1vallem  32435  hdmapffval  32466  hdmapfval  32467  hdmapval  32468  hdmapevec2  32476  hgmapffval  32525  hgmapfval  32526  hgmapval  32527  hdmaplna2  32550  hdmapglnm2  32551  hdmapinvlem3  32560  hlhilset  32574  hlhilipval  32589
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-uni 4008  df-br 4205  df-iota 5409  df-fv 5453
  Copyright terms: Public domain W3C validator