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

Theorem fveq1 5727
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )

Proof of Theorem fveq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq 4214 . . 3  |-  ( F  =  G  ->  ( A F x  <->  A G x ) )
21iotabidv 5439 . 2  |-  ( F  =  G  ->  ( iota x A F x )  =  ( iota
x A G x ) )
3 df-fv 5462 . 2  |-  ( F `
 A )  =  ( iota x A F x )
4 df-fv 5462 . 2  |-  ( G `
 A )  =  ( iota x A G x )
52, 3, 43eqtr4g 2493 1  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4212   iotacio 5416   ` cfv 5454
This theorem is referenced by:  fveq1i  5729  fveq1d  5730  fvmptdf  5816  fvmptdv2  5818  isoeq1  6039  oveq  6087  offval  6312  ofrfval  6313  offval3  6318  bropopvvv  6426  smoeq  6612  recseq  6634  tfrlem3  6638  tfrlem3a  6639  tfrlem12  6650  tz7.44-2  6665  tz7.44-3  6666  rdgeq1  6669  mapsncnv  7060  elixp2  7066  resixpfo  7100  elixpsn  7101  mapsnen  7184  mapxpen  7273  ac6sfi  7351  ordtypelem7  7493  wemaplem1  7515  ixpiunwdom  7559  oemapval  7639  cantnf  7649  wemapwe  7654  cnfcom3clem  7662  infxpenc2lem2  7901  fseqenlem1  7905  dfac8clem  7913  ac5num  7917  acni  7926  acni2  7927  acnlem  7929  dfac4  8003  dfac5lem5  8008  dfac2a  8010  dfac9  8016  dfacacn  8021  dfac12lem1  8023  dfac12r  8026  cofsmo  8149  cfsmolem  8150  cfsmo  8151  cfcoflem  8152  coftr  8153  alephsing  8156  isfin3ds  8209  fin23lem17  8218  fin23lem32  8224  fin23lem39  8230  isf33lem  8246  isf34lem6  8260  axcc2lem  8316  axcc3  8318  axdc2lem  8328  axdc3lem2  8331  axdc3lem3  8332  axdc3  8334  axdc4lem  8335  axcclem  8337  ac6num  8359  axdclem2  8400  konigthlem  8443  inar1  8650  1fv  11120  axdc4uzlem  11321  seqeq3  11328  seqof  11380  ccatfval  11742  clim  12288  rlim  12289  ello1  12309  elo1  12320  summo  12511  fsum  12514  vdwlem6  13354  vdwlem8  13356  ramcl  13397  strfvnd  13484  prdsplusgval  13695  prdsmulrval  13697  prdsleval  13699  prdsdsval  13700  prdsvscaval  13701  xpsff1o  13793  isacs2  13878  isnat  14144  yonedalem3b  14376  yonedainv  14378  ismhm  14740  prdspjmhm  14766  isgrpinv  14855  pwsmulg  14932  isghm  15006  cayleylem2  15111  efgsdm  15362  efgredlemd  15376  efgredlem  15379  efgred  15380  efgrelexlema  15381  efgrelexlemb  15382  prdsgsum  15552  isabv  15907  islmhm  16103  psrmulfval  16449  evlslem2  16568  coe1fval  16603  coe1mul2lem2  16661  coe1tm  16665  frgpcyg  16854  iscnp  17301  1stcfb  17508  ptpjpre1  17603  elpt  17604  elptr  17605  ptpjopn  17644  dfac14  17650  upxp  17655  pthaus  17670  ptrescn  17671  xkoptsub  17686  cnmptkp  17712  xkofvcn  17716  cnmptk1p  17717  cnmptk2  17718  ptunhmeo  17840  ptcmplem3  18085  ptcmplem4  18086  symgtgp  18131  prdstmdd  18153  isucn  18308  imasdsf1olem  18403  prdsxmslem2  18559  nmoval  18749  elcncf  18919  ishtpy  18997  pcoval  19036  om1elbas  19057  elpi1i  19071  iscau  19229  mbfi1fseqlem6  19612  mbfi1flimlem  19614  isibl  19657  evlslem3  19935  evlslem1  19936  mpfrcl  19939  deg1ldg  20015  deg1leb  20018  elply2  20115  elplyr  20120  ne0p  20126  coeeu  20144  coelem  20145  coeeq  20146  coeidlem  20156  elqaalem3  20238  qaa  20240  iaa  20242  aareccl  20243  aannenlem2  20246  aaliou2  20257  dchrptlem2  21049  dchrpt  21051  dchrsum2  21052  sumdchr2  21054  dchrvmaeq0  21198  rpvmasum2  21206  dchrisum0re  21207  ostth  21333  wlks  21526  iswlk  21527  iswlkon  21531  istrl  21537  constr1trl  21588  2wlklem1  21597  iscrct  21611  iscycl  21612  constr3cyclpe  21650  iseupa  21687  ex-fv  21751  elghomlem2  21950  isnvlem  22089  islno  22254  nmooval  22264  nmblolbi  22301  isphg  22318  ajmoi  22360  ajval  22363  ubthlem3  22374  htthlem  22420  hcau  22686  hlimi  22690  hosmval  23238  hommval  23239  hodmval  23240  hfsmval  23241  hfmmval  23242  adjmo  23335  nmopval  23359  elcnop  23360  ellnop  23361  elunop  23375  elhmop  23376  nmfnval  23379  elcnfn  23385  ellnfn  23386  adjeu  23392  adjval  23393  eigvecval  23399  eigvalfval  23400  adj1  23436  adjeq  23438  hmopadj2  23444  lnopeq0i  23510  lnopeq  23512  elunop2  23516  lnophm  23522  hmopco  23526  nmbdoplb  23528  nmcoplb  23533  lnopcon  23538  lnfn0  23550  lnfnmul  23551  nmbdfnlb  23553  nmcfnlb  23557  lnfncon  23559  riesz4  23567  riesz1  23568  cnlnadjlem9  23578  cnlnadjeu  23581  cnlnssadj  23583  nmopcoi  23598  bra11  23611  cnvbraval  23613  pjss2coi  23667  pjssdif2i  23677  pjssdif1i  23678  pjclem4  23702  pj3si  23710  pj3cor1i  23712  isst  23716  ishst  23717  stri  23760  hstri  23768  ismeas  24553  isrnmeas  24554  cntnevol  24582  sitgval  24647  cndprobval  24691  derangenlem  24857  subfacp1lem3  24868  subfacp1lem5  24870  subfacp1lem6  24871  subfacp1  24872  sconpht  24916  cnpcon  24917  txpcon  24919  ptpcon  24920  indispcon  24921  conpcon  24922  cvxpcon  24929  cvmliftmo  24971  cvmliftlem14  24984  cvmliftlem15  24985  cvmliftiota  24988  cvmlift2  25003  cvmliftphtlem  25004  cvmlift3lem2  25007  cvmlift3lem6  25011  cvmlift3lem7  25012  cvmlift3lem9  25014  cvmlift3  25015  dfrtrclrec2  25143  rtrclreclem.refl  25144  rtrclreclem.subset  25145  rtrclreclem.min  25147  dfrtrcl2  25148  shftvalg  25208  prodmo  25262  fprod  25267  poseq  25528  soseq  25529  wfrlem1  25538  wfrlem15  25552  frrlem1  25582  sltval  25602  nobndlem6  25652  brbtwn  25838  brbtwn2  25844  colinearalg  25849  axsegconlem1  25856  axsegcon  25866  ax5seglem5  25872  axpasch  25880  axlowdim  25900  axeuclidlem  25901  axcontlem1  25903  axcontlem2  25904  axcontlem5  25907  bpolylem  26094  bpolyval  26095  voliunnfl  26250  volsupnfl  26251  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  ftc1anclem5  26284  eqfnun  26423  upixp  26431  fdc  26449  isismty  26510  rrnmval  26537  isrngohom  26581  ismrc  26755  mzpclval  26782  mzpsubst  26805  mzprename  26806  mzpcompact2lem  26808  eldioph  26816  eldioph2  26820  eldioph2b  26821  eldioph3  26824  rexrabdioph  26854  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  eldioph4i  26873  rabren3dioph  26876  mzpcong  27037  jm2.27dlem1  27080  wepwsolem  27116  aomclem6  27134  aomclem8  27136  dfac11  27137  dsmmelbas  27182  uvcf1  27218  enfixsn  27234  islindf  27259  islindf4  27285  dgraalem  27327  dgraaub  27330  dgraa0p  27331  mpaaeu  27332  mpaalem  27334  aaitgo  27344  rngunsnply  27355  psgnunilem2  27395  psgnunilem3  27396  dvconstbi  27528  addrval  27647  subrval  27648  mulvval  27649  fnchoice  27676  refsum2cnlem1  27684  fmulcl  27687  fmuldfeqlem1  27688  stoweidlem2  27727  stoweidlem6  27731  stoweidlem8  27733  stoweidlem9  27734  stoweidlem15  27740  stoweidlem16  27741  stoweidlem17  27742  stoweidlem18  27743  stoweidlem21  27746  stoweidlem27  27752  stoweidlem31  27756  stoweidlem36  27761  stoweidlem37  27762  stoweidlem41  27766  stoweidlem43  27768  stoweidlem44  27769  stoweidlem45  27770  stoweidlem46  27771  stoweidlem48  27773  stoweidlem51  27776  stoweidlem55  27780  stoweidlem59  27784  stoweidlem60  27785  stoweidlem62  27787  cshweqrep  28274  wlkelwrd  28295  wlkcompim  28302  usg2wlk  28319  bnj66  29231  bnj106  29239  bnj125  29243  bnj154  29249  bnj155  29250  bnj526  29259  bnj540  29263  bnj609  29288  bnj611  29289  bnj893  29299  bnj1000  29312  bnj1014  29331  bnj1015  29332  bnj1234  29382  bnj1463  29424  islfl  29858  isopos  29978  islaut  30880  ispautN  30896  isldil  30907  isltrn  30916  ltrnid  30932  ltrneq2  30945  isdilN  30951  istrnN  30954  trlval  30959  ltrneq3  31005  cdleme50ex  31356  cdleme  31357  cdlemg1a  31367  ltrniotaval  31378  ltrniotavalbN  31381  cdlemeiota  31382  cdlemg2jlemOLDN  31390  cdlemg2fvlem  31391  cdlemg2klem  31392  istendo  31557  tendoplcbv  31572  tendopl  31573  tendoicbv  31590  tendoi  31591  tendoid0  31622  tendo1ne0  31625  cdlemksv2  31644  cdlemkuv2  31664  cdlemk33N  31706  cdlemk34  31707  cdlemk36  31710  cdlemk19u  31767  cdlemk  31771  tendoex  31772  dvavsca  31814  dvhvscacbv  31896  dvhvscaval  31897  dicopelval  31975  dicelval1sta  31985  diclspsn  31992  dihmeetlem13N  32117  dih1dimatlem0  32126  dih1dimatlem  32127  dihpN  32134  islpolN  32281  hdmap1fval  32595  hdmapfval  32628
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462
  Copyright terms: Public domain W3C validator