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

Theorem fveq1 6407
Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
fveq1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))

Proof of Theorem fveq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq 4846 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 6085 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 6109 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 6109 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2865 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4844  cio 6062  cfv 6101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109
This theorem is referenced by:  fveq1i  6409  fveq1d  6410  iffv  6425  fvmptd3f  6516  fvmptdv2  6519  fsnex  6762  f1prex  6763  isoeq1  6791  oveq  6880  elovmpt3imp  7120  offval  7134  ofrfval  7135  offval3  7392  bropopvvv  7489  bropfvvvvlem  7490  wfrlem1  7649  wfrlem3a  7652  wfrlem15  7665  smoeq  7683  tfrlem12  7721  tz7.44-2  7739  tz7.44-3  7740  rdgeq1  7743  mapsncnv  8141  elixp2  8149  resixpfo  8183  elixpsn  8184  mapsnend  8271  enfixsn  8308  mapxpen  8365  ac6sfi  8443  ordtypelem7  8668  wemaplem1  8690  ixpiunwdom  8735  oemapval  8827  cantnf  8837  wemapwe  8841  cnfcom3clem  8849  updjud  9043  infxpenc2lem2  9126  fseqenlem1  9130  dfac8clem  9138  ac5num  9142  acni  9151  acni2  9152  acnlem  9154  dfac4  9228  dfac5lem5  9233  dfac2a  9235  dfac9  9243  dfacacn  9248  dfac12lem1  9250  dfac12r  9253  cofsmo  9376  cfsmolem  9377  cfsmo  9378  cfcoflem  9379  coftr  9380  alephsing  9383  isfin3ds  9436  fin23lem17  9445  fin23lem32  9451  fin23lem39  9457  isf33lem  9473  isf34lem6  9487  axcc2lem  9543  axcc3  9545  axdc2lem  9555  axdc3lem2  9558  axdc3lem3  9559  axdc3  9561  axdc4lem  9562  axcclem  9564  ac6num  9586  axdclem2  9627  konigthlem  9675  inar1  9882  1fv  12682  axdc4uzlem  13006  seqeq3  13029  seqof  13081  ccatfval  13570  wrdl1s1  13609  ccat1st1st  13626  cshf1  13780  cshweqrep  13791  wrdlen2i  13911  wwlktovf  13924  wwlktovf1  13925  wwlktovfo  13926  wrd2f1tovbij  13928  dfrtrclrec2  14020  rtrclreclem1  14021  rtrclreclem2  14022  rtrclreclem4  14024  dfrtrcl2  14025  clim  14448  rlim  14449  ello1  14469  elo1  14480  summo  14671  fsum  14674  prodmo  14887  fprod  14892  bpolylem  14999  bpolyval  15000  vdwlem6  15907  vdwlem8  15909  ramcl  15950  strfvnd  16087  prdsplusgval  16338  prdsmulrval  16340  prdsleval  16342  prdsdsval  16343  prdsvscaval  16344  xpsff1o  16433  isacs2  16518  isnat  16811  yonedalem3b  17124  yonedainv  17126  ismhm  17542  prdspjmhm  17572  isgrpinv  17677  pwsmulg  17789  isghm  17862  cayleylem2  18034  symgfix2  18037  gsmsymgrfix  18049  gsmsymgreq  18053  symgfixelq  18054  pmtr3ncomlem2  18095  pmtrdifel  18101  pmtrdifwrdel  18106  pmtrdifwrdel2  18107  psgnunilem2  18116  psgnunilem3  18117  efgsdm  18344  efgredlemd  18358  efgredlem  18361  efgred  18362  efgrelexlema  18363  efgrelexlemb  18364  prdsgsum  18578  isabv  19023  islmhm  19234  psrmulfval  19594  evlslem2  19720  evlslem3  19722  evlslem1  19723  mpfrcl  19726  coe1fval  19783  coe1mul2lem2  19846  coe1tm  19851  frgpcyg  20129  psgndiflemB  20154  psgndiflemA  20155  dsmmelbas  20293  frlmipval  20328  frlmphl  20330  uvcf1  20341  islindf  20361  islindf4  20387  madetsumid  20478  mvmulval  20560  marepvval0  20583  mulmarep1gsum2  20591  mdetleib2  20605  m1detdiag  20614  mdetralt  20625  mdetunilem7  20635  mdetunilem9  20637  m2detleiblem3  20646  m2detleiblem4  20647  m2detleib  20648  symgmatr01lem  20671  gsummatr01lem1  20673  gsummatr01lem4  20676  gsummatr01  20677  smadiadetlem3  20686  pmatcoe1fsupp  20719  pmatcollpw3lem  20801  pmatcollpw3fi1lem2  20805  iscnp  21255  1stcfb  21462  ptpjpre1  21588  elpt  21589  elptr  21590  ptpjopn  21629  dfac14  21635  upxp  21640  pthaus  21655  ptrescn  21656  xkoptsub  21671  cnmptkp  21697  xkofvcn  21701  cnmptk1p  21702  cnmptk2  21703  ptunhmeo  21825  ptcmplem3  22071  ptcmplem4  22072  symgtgp  22118  prdstmdd  22140  isucn  22295  imasdsf1olem  22391  prdsxmslem2  22547  tngngp3  22673  nmoval  22732  elcncf  22905  ishtpy  22984  pcoval  23023  om1elbas  23044  elpi1i  23058  iscau  23286  rrxds  23393  mbfi1fseqlem6  23701  mbfi1flimlem  23703  isibl  23746  deg1ldg  24066  deg1leb  24069  elply2  24166  elplyr  24171  ne0p  24177  coeeu  24195  coelem  24196  coeeq  24197  coeidlem  24207  elqaalem3  24290  qaa  24292  iaa  24294  aareccl  24295  aannenlem2  24298  aaliou2  24309  dchrptlem2  25204  dchrpt  25206  dchrsum2  25207  sumdchr2  25209  dchrvmaeq0  25407  rpvmasum2  25415  dchrisum0re  25416  ostth  25542  iscgrg  25621  isismt  25643  israg  25806  iseqlg  25961  brbtwn  25993  brbtwn2  25999  colinearalg  26004  axsegconlem1  26011  axsegcon  26021  ax5seglem5  26027  axpasch  26035  axlowdim  26055  axeuclidlem  26056  axcontlem1  26058  axcontlem2  26059  axcontlem5  26062  vtxdgfval  26591  1egrvtxdg1  26633  isewlk  26726  iswlk  26734  uspgr2wlkeq2  26771  iswlkon  26781  isclwlk  26897  iscrct  26914  iscycl  26915  iswwlks  26957  wwlknon  26981  wwlknonOLD  26983  wlkiswwlks2  27002  wlkwwlkfunOLD  27023  wlkwwlksurOLD  27025  wlkwwlkbij2OLD  27027  wwlksnredwwlkn0  27033  wlksnwwlknvbij  27045  wlksnwwlknvbijOLD  27046  wwlksnextproplem3  27049  wwlksnextprop  27050  umgr2wlk  27089  midwwlks2s3  27092  elwwlks2  27108  elwspths2spth  27109  rusgrnumwwlkslem  27111  rusgrnumwwlkb0  27113  rusgrnumwwlks  27116  isclwwlk  27127  clwlkclwwlklem1  27142  clwwlkn1loopb  27192  clwwlkel  27195  clwwlkf  27196  clwwlkf1  27198  isclwwlknon  27257  isclwwlknonOLD  27258  clwwlknon1  27265  s2elclwwlknon2  27272  clwwlkvbij  27282  clwwlkvbijOLDOLD  27283  clwwlkvbijOLD  27284  clwwlknunOLD  27286  uhgr3cyclex  27355  fusgreg2wsplem  27508  fusgr2wsp2nb  27509  fusgreghash2wsp  27513  2clwwlkel  27526  numclwwlkovgelOLD  27529  extwwlkfabel  27532  numclwwlk1lem2fv  27535  numclwwlk1lem2  27539  numclwwlk1lem2OLD  27540  clwwlknonclwlknonf1o  27542  dlwwlknondlwlknonf1o  27545  numclwwlk2lem1  27556  numclwlk2lem2f  27557  numclwlk2lem2f1o  27559  numclwwlk2lem1OLD  27563  numclwlk2lem2fOLD  27564  numclwlk2lem2f1oOLD  27566  ex-fv  27631  isnvlem  27793  islno  27936  nmooval  27946  nmblolbi  27983  isphg  28000  ajmoi  28042  ajval  28045  ubthlem3  28056  htthlem  28102  hcau  28369  hlimi  28373  hosmval  28922  hommval  28923  hodmval  28924  hfsmval  28925  hfmmval  28926  adjmo  29019  nmopval  29043  elcnop  29044  ellnop  29045  elunop  29059  elhmop  29060  nmfnval  29063  elcnfn  29069  ellnfn  29070  adjeu  29076  adjval  29077  eigvecval  29083  eigvalfval  29084  adj1  29120  adjeq  29122  hmopadj2  29128  lnopeq0i  29194  lnopeq  29196  elunop2  29200  lnophm  29206  hmopco  29210  nmbdoplb  29212  nmcoplb  29217  lnopcon  29222  lnfn0  29234  lnfnmul  29235  nmbdfnlb  29237  nmcfnlb  29241  lnfncon  29243  riesz4  29251  riesz1  29252  cnlnadjlem9  29262  cnlnadjeu  29265  cnlnssadj  29267  nmopcoi  29282  bra11  29295  cnvbraval  29297  pjss2coi  29351  pjssdif2i  29361  pjssdif1i  29362  pjclem4  29386  pj3si  29394  pj3cor1i  29396  isst  29400  ishst  29401  stri  29444  hstri  29452  aciunf1lem  29789  lmatval  30204  mdetpmtr1  30214  ismeas  30587  isrnmeas  30588  cntnevol  30616  carsgval  30690  sitgval  30719  eulerpartleme  30750  eulerpartlemd  30753  eulerpartlemr  30761  eulerpartlemgvv  30763  eulerpart  30769  cndprobval  30820  signstfvneq0  30974  reprsum  31016  reprsuc  31018  reprpmtf1o  31029  reprdifc  31030  breprexp  31036  vtsval  31040  hgt750lemb  31059  hgt750lema  31060  hgt750leme  31061  bnj66  31253  bnj106  31261  bnj125  31265  bnj154  31271  bnj155  31272  bnj526  31281  bnj540  31285  bnj609  31310  bnj611  31311  bnj893  31321  bnj1000  31334  bnj1014  31353  bnj1015  31354  bnj1234  31404  bnj1463  31446  derangenlem  31476  subfacp1lem3  31487  subfacp1lem5  31489  subfacp1lem6  31490  subfacp1  31491  sconnpht  31534  cnpconn  31535  txpconn  31537  ptpconn  31538  indispconn  31539  connpconn  31540  cvxpconn  31547  cvmliftmo  31589  cvmliftlem14  31602  cvmliftlem15  31603  cvmliftiota  31606  cvmlift2  31621  cvmliftphtlem  31622  cvmlift3lem2  31625  cvmlift3lem6  31629  cvmlift3lem7  31630  cvmlift3lem9  31632  cvmlift3  31633  mrsubff1  31734  mrsub0  31736  mrsubccat  31738  mrsubcn  31739  elmsubrn  31748  msubrn  31749  msubco  31751  msubvrs  31780  mclsax  31789  shftvalg  31939  poseq  32074  soseq  32075  frrlem1  32101  sltval  32121  nolesgn2o  32145  noresle  32167  noprefixmo  32169  nosupfv  32173  fwddifval  32590  fwddifnval  32591  bj-evalval  33338  unceq  33699  matunitlindflem2  33719  poimirlem17  33739  poimirlem20  33742  poimirlem22  33744  poimirlem23  33745  poimirlem27  33749  poimirlem28  33750  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  poimir  33755  broucube  33756  voliunnfl  33766  volsupnfl  33767  itg2addnclem  33773  itg2addnclem3  33775  itg2addnc  33776  ftc1anclem2  33798  ftc1anclem5  33801  eqfnun  33828  upixp  33836  fdc  33852  isismty  33911  rrnmval  33938  elghomlem2OLD  33996  isrngohom  34075  islfl  34840  isopos  34960  islaut  35863  ispautN  35879  isldil  35890  isltrn  35899  ltrnid  35915  ltrneq2  35928  isdilN  35935  istrnN  35938  trlval  35943  ltrneq3  35989  cdleme50ex  36340  cdleme  36341  cdlemg1a  36351  ltrniotaval  36362  ltrniotavalbN  36365  cdlemeiota  36366  cdlemg2jlemOLDN  36374  cdlemg2fvlem  36375  cdlemg2klem  36376  istendo  36541  tendoplcbv  36556  tendopl  36557  tendoicbv  36574  tendoi  36575  tendoid0  36606  tendo1ne0  36609  cdlemksv2  36628  cdlemkuv2  36648  cdlemk33N  36690  cdlemk34  36691  cdlemk36  36694  cdlemk19u  36751  cdlemk  36755  tendoex  36756  dvavsca  36798  dvhvscacbv  36879  dvhvscaval  36880  dicopelval  36958  dicelval1sta  36968  diclspsn  36975  dihmeetlem13N  37100  dih1dimatlem0  37109  dih1dimatlem  37110  dihpN  37117  islpolN  37264  hdmap1fval  37577  hdmapfval  37608  ismrc  37766  mzpclval  37790  mzpsubst  37813  mzprename  37814  mzpcompact2lem  37816  eldioph  37823  eldioph2  37827  eldioph2b  37828  eldioph3  37831  rexrabdioph  37860  2rexfrabdioph  37862  3rexfrabdioph  37863  4rexfrabdioph  37864  6rexfrabdioph  37865  7rexfrabdioph  37866  eldioph4i  37878  rabren3dioph  37881  mzpcong  38040  jm2.27dlem1  38077  wepwsolem  38113  aomclem6  38130  aomclem8  38132  dfac11  38133  dgraalem  38216  dgraaub  38219  dgraa0p  38220  mpaaeu  38221  mpaalem  38223  aaitgo  38233  rngunsnply  38244  eliunov2  38471  rfovcnvfvd  38801  fsovfvd  38804  fsovcnvlem  38807  dssmapfv2d  38812  dssmapnvod  38814  clsk1independent  38844  ntrclskb  38867  ntrclsk13  38869  gneispace2  38930  dvconstbi  39033  addrval  39168  subrval  39169  mulvval  39170  fnchoice  39682  refsum2cnlem1  39690  choicefi  39879  axccdom  39903  fmulcl  40293  fmuldfeqlem1  40294  mccllem  40309  mccl  40310  climf  40334  climf2  40378  dvnprodlem1  40641  dvnprodlem3  40643  dvnprod  40644  stoweidlem2  40698  stoweidlem6  40702  stoweidlem8  40704  stoweidlem9  40705  stoweidlem15  40711  stoweidlem16  40712  stoweidlem17  40713  stoweidlem18  40714  stoweidlem21  40717  stoweidlem27  40723  stoweidlem31  40727  stoweidlem36  40732  stoweidlem37  40733  stoweidlem41  40737  stoweidlem43  40739  stoweidlem44  40740  stoweidlem45  40741  stoweidlem46  40742  stoweidlem48  40744  stoweidlem51  40747  stoweidlem55  40751  stoweidlem59  40755  stoweidlem60  40756  stoweidlem62  40758  fourierdlem2  40805  fourierdlem3  40806  elaa2lem  40929  etransclem11  40941  etransclem24  40954  etransclem26  40956  etransclem28  40958  etransclem35  40965  rrndistlt  40989  ioorrnopn  41004  subsaliuncllem  41054  sge0val  41062  ismea  41147  caragenval  41189  isome  41190  isomenndlem  41226  hoicvrrex  41252  ovnlecvr  41254  ovncvrrp  41260  ovn0lem  41261  ovnsubaddlem1  41266  ovnsubadd  41268  hsphoif  41272  hoidmvval  41273  hsphoival  41275  hoidmvlelem3  41293  hoidmvlelem5  41295  hoidmvle  41296  ovnhoilem1  41297  ovnhoi  41299  ovnlecvr2  41306  ovncvr2  41307  hoidifhspval2  41311  hoiqssbllem2  41319  hspmbllem2  41323  hspmbllem3  41324  hspmbl  41325  ovnovollem1  41352  smfmullem2  41481  smfmul  41484  smfpimcclem  41495  iccpart  41927  iccpartiun  41945  icceuelpart  41947  nnsum3primes4  42251  nnsum3primesgbe  42255  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbnd  42272  isupwlk  42285  ismgmhm  42351  isrnghm  42460  lincval  42766  lincdifsn  42781  linindslinci  42805  lindslinindsimp1  42814  linds0  42822  el0ldep  42823  lindsrng01  42825  snlindsntorlem  42827  ldepspr  42830  islindeps2  42840  zlmodzxzldep  42861  offval0  42867  bigoval  42911  elbigo  42913  setrecseq  43000  aacllem  43118
  Copyright terms: Public domain W3C validator