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

Theorem fveq1 6228
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 4687 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 5910 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 5934 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5934 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2710 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523   class class class wbr 4685  cio 5887  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934
This theorem is referenced by:  fveq1i  6230  fveq1d  6231  iffv  6243  fvmptd3f  6334  fvmptdv2  6337  fsnex  6578  f1prex  6579  isoeq1  6607  oveq  6696  elovmpt3imp  6932  offval  6946  ofrfval  6947  offval3  7204  bropopvvv  7300  bropfvvvvlem  7301  wfrlem1  7459  wfrlem3a  7462  wfrlem15  7474  smoeq  7492  tfrlem12  7530  tz7.44-2  7548  tz7.44-3  7549  rdgeq1  7552  mapsncnv  7946  elixp2  7954  resixpfo  7988  elixpsn  7989  mapsnen  8076  enfixsn  8110  mapxpen  8167  ac6sfi  8245  ordtypelem7  8470  wemaplem1  8492  ixpiunwdom  8537  oemapval  8618  cantnf  8628  wemapwe  8632  cnfcom3clem  8640  infxpenc2lem2  8881  fseqenlem1  8885  dfac8clem  8893  ac5num  8897  acni  8906  acni2  8907  acnlem  8909  dfac4  8983  dfac5lem5  8988  dfac2a  8990  dfac9  8996  dfacacn  9001  dfac12lem1  9003  dfac12r  9006  cofsmo  9129  cfsmolem  9130  cfsmo  9131  cfcoflem  9132  coftr  9133  alephsing  9136  isfin3ds  9189  fin23lem17  9198  fin23lem32  9204  fin23lem39  9210  isf33lem  9226  isf34lem6  9240  axcc2lem  9296  axcc3  9298  axdc2lem  9308  axdc3lem2  9311  axdc3lem3  9312  axdc3  9314  axdc4lem  9315  axcclem  9317  ac6num  9339  axdclem2  9380  konigthlem  9428  inar1  9635  1fv  12497  axdc4uzlem  12822  seqeq3  12846  seqof  12898  ccatfval  13391  wrdl1s1  13431  ccat1st1st  13448  cshf1  13602  cshweqrep  13613  wrdlen2i  13732  wwlktovf  13745  wwlktovf1  13746  wwlktovfo  13747  wrd2f1tovbij  13749  dfrtrclrec2  13841  rtrclreclem1  13842  rtrclreclem2  13843  rtrclreclem4  13845  dfrtrcl2  13846  clim  14269  rlim  14270  ello1  14290  elo1  14301  summo  14492  fsum  14495  prodmo  14710  fprod  14715  bpolylem  14823  bpolyval  14824  vdwlem6  15737  vdwlem8  15739  ramcl  15780  strfvnd  15923  prdsplusgval  16180  prdsmulrval  16182  prdsleval  16184  prdsdsval  16185  prdsvscaval  16186  xpsff1o  16275  isacs2  16361  isnat  16654  yonedalem3b  16966  yonedainv  16968  ismhm  17384  prdspjmhm  17414  isgrpinv  17519  pwsmulg  17634  isghm  17707  cayleylem2  17879  symgfix2  17882  gsmsymgrfix  17894  gsmsymgreq  17898  symgfixelq  17899  pmtr3ncomlem2  17940  pmtrdifel  17946  pmtrdifwrdel  17951  pmtrdifwrdel2  17952  psgnunilem2  17961  psgnunilem3  17962  efgsdm  18189  efgredlemd  18203  efgredlem  18206  efgred  18207  efgrelexlema  18208  efgrelexlemb  18209  prdsgsum  18423  isabv  18867  islmhm  19075  psrmulfval  19433  evlslem2  19560  evlslem3  19562  evlslem1  19563  mpfrcl  19566  coe1fval  19623  coe1mul2lem2  19686  coe1tm  19691  frgpcyg  19970  psgndiflemB  19994  psgndiflemA  19995  dsmmelbas  20131  frlmipval  20166  frlmphl  20168  uvcf1  20179  islindf  20199  islindf4  20225  madetsumid  20315  mvmulval  20397  marepvval0  20420  mulmarep1gsum2  20428  mdetleib2  20442  m1detdiag  20451  mdetralt  20462  mdetunilem7  20472  mdetunilem9  20474  m2detleiblem3  20483  m2detleiblem4  20484  m2detleib  20485  symgmatr01lem  20507  gsummatr01lem1  20509  gsummatr01lem4  20512  gsummatr01  20513  smadiadetlem3  20522  pmatcoe1fsupp  20554  pmatcollpw3lem  20636  pmatcollpw3fi1lem2  20640  iscnp  21089  1stcfb  21296  ptpjpre1  21422  elpt  21423  elptr  21424  ptpjopn  21463  dfac14  21469  upxp  21474  pthaus  21489  ptrescn  21490  xkoptsub  21505  cnmptkp  21531  xkofvcn  21535  cnmptk1p  21536  cnmptk2  21537  ptunhmeo  21659  ptcmplem3  21905  ptcmplem4  21906  symgtgp  21952  prdstmdd  21974  isucn  22129  imasdsf1olem  22225  prdsxmslem2  22381  tngngp3  22507  nmoval  22566  elcncf  22739  ishtpy  22818  pcoval  22857  om1elbas  22878  elpi1i  22892  iscau  23120  rrxds  23227  mbfi1fseqlem6  23532  mbfi1flimlem  23534  isibl  23577  deg1ldg  23897  deg1leb  23900  elply2  23997  elplyr  24002  ne0p  24008  coeeu  24026  coelem  24027  coeeq  24028  coeidlem  24038  elqaalem3  24121  qaa  24123  iaa  24125  aareccl  24126  aannenlem2  24129  aaliou2  24140  dchrptlem2  25035  dchrpt  25037  dchrsum2  25038  sumdchr2  25040  dchrvmaeq0  25238  rpvmasum2  25246  dchrisum0re  25247  ostth  25373  iscgrg  25452  isismt  25474  israg  25637  iseqlg  25792  brbtwn  25824  brbtwn2  25830  colinearalg  25835  axsegconlem1  25842  axsegcon  25852  ax5seglem5  25858  axpasch  25866  axlowdim  25886  axeuclidlem  25887  axcontlem1  25889  axcontlem2  25890  axcontlem5  25893  vtxdgfval  26419  1egrvtxdg1  26461  isewlk  26554  iswlk  26562  uspgr2wlkeq2  26599  iswlkon  26609  isclwlk  26725  iscrct  26741  iscycl  26742  iswwlks  26784  wwlknon  26808  wwlknonOLD  26810  wlkiswwlks2  26829  wlkwwlkfun  26849  wlkwwlksur  26851  wlkwwlkbij2  26853  wwlksnredwwlkn0  26859  wlksnwwlknvbij  26871  wwlksnextproplem3  26874  wwlksnextprop  26875  umgr2wlk  26914  midwwlks2s3  26917  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlkslem  26936  rusgrnumwwlkb0  26938  rusgrnumwwlks  26941  isclwwlk  26952  clwlkclwwlklem1  26965  clwwlkn1loopb  27006  clwwlkel  27009  clwwlkf  27010  clwwlkf1  27012  isclwwlknon  27065  isclwwlknonOLD  27066  clwwlknon1  27072  clwwlkvbij  27088  clwwlkvbijOLD  27089  clwwlknunOLD  27091  uhgr3cyclex  27160  fusgreg2wsplem  27313  fusgr2wsp2nb  27314  fusgreghash2wsp  27318  2clwwlkel  27337  numclwwlkovgelOLD  27340  extwwlkfabel  27343  numclwlk1lem2fv  27346  numclwlk1lem2  27350  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  ex-fv  27430  isnvlem  27593  islno  27736  nmooval  27746  nmblolbi  27783  isphg  27800  ajmoi  27842  ajval  27845  ubthlem3  27856  htthlem  27902  hcau  28169  hlimi  28173  hosmval  28722  hommval  28723  hodmval  28724  hfsmval  28725  hfmmval  28726  adjmo  28819  nmopval  28843  elcnop  28844  ellnop  28845  elunop  28859  elhmop  28860  nmfnval  28863  elcnfn  28869  ellnfn  28870  adjeu  28876  adjval  28877  eigvecval  28883  eigvalfval  28884  adj1  28920  adjeq  28922  hmopadj2  28928  lnopeq0i  28994  lnopeq  28996  elunop2  29000  lnophm  29006  hmopco  29010  nmbdoplb  29012  nmcoplb  29017  lnopcon  29022  lnfn0  29034  lnfnmul  29035  nmbdfnlb  29037  nmcfnlb  29041  lnfncon  29043  riesz4  29051  riesz1  29052  cnlnadjlem9  29062  cnlnadjeu  29065  cnlnssadj  29067  nmopcoi  29082  bra11  29095  cnvbraval  29097  pjss2coi  29151  pjssdif2i  29161  pjssdif1i  29162  pjclem4  29186  pj3si  29194  pj3cor1i  29196  isst  29200  ishst  29201  stri  29244  hstri  29252  aciunf1lem  29590  lmatval  30007  mdetpmtr1  30017  ismeas  30390  isrnmeas  30391  cntnevol  30419  carsgval  30493  sitgval  30522  eulerpartleme  30553  eulerpartlemd  30556  eulerpartlemr  30564  eulerpartlemgvv  30566  eulerpart  30572  cndprobval  30623  signstfvneq0  30777  reprsum  30819  reprsuc  30821  reprpmtf1o  30832  reprdifc  30833  breprexp  30839  vtsval  30843  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  bnj66  31056  bnj106  31064  bnj125  31068  bnj154  31074  bnj155  31075  bnj526  31084  bnj540  31088  bnj609  31113  bnj611  31114  bnj893  31124  bnj1000  31137  bnj1014  31156  bnj1015  31157  bnj1234  31207  bnj1463  31249  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  subfacp1  31294  sconnpht  31337  cnpconn  31338  txpconn  31340  ptpconn  31341  indispconn  31342  connpconn  31343  cvxpconn  31350  cvmliftmo  31392  cvmliftlem14  31405  cvmliftlem15  31406  cvmliftiota  31409  cvmlift2  31424  cvmliftphtlem  31425  cvmlift3lem2  31428  cvmlift3lem6  31432  cvmlift3lem7  31433  cvmlift3lem9  31435  cvmlift3  31436  mrsubff1  31537  mrsub0  31539  mrsubccat  31541  mrsubcn  31542  elmsubrn  31551  msubrn  31552  msubco  31554  msubvrs  31583  mclsax  31592  shftvalg  31743  poseq  31878  soseq  31879  frrlem1  31905  sltval  31925  nolesgn2o  31949  noresle  31971  noprefixmo  31973  nosupfv  31977  fwddifval  32394  fwddifnval  32395  bj-evalval  33152  unceq  33516  matunitlindflem2  33536  poimirlem17  33556  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem27  33566  poimirlem28  33567  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  poimir  33572  broucube  33573  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  ftc1anclem2  33616  ftc1anclem5  33619  eqfnun  33646  upixp  33654  fdc  33671  isismty  33730  rrnmval  33757  elghomlem2OLD  33815  isrngohom  33894  islfl  34665  isopos  34785  islaut  35687  ispautN  35703  isldil  35714  isltrn  35723  ltrnid  35739  ltrneq2  35752  isdilN  35759  istrnN  35762  trlval  35767  ltrneq3  35813  cdleme50ex  36164  cdleme  36165  cdlemg1a  36175  ltrniotaval  36186  ltrniotavalbN  36189  cdlemeiota  36190  cdlemg2jlemOLDN  36198  cdlemg2fvlem  36199  cdlemg2klem  36200  istendo  36365  tendoplcbv  36380  tendopl  36381  tendoicbv  36398  tendoi  36399  tendoid0  36430  tendo1ne0  36433  cdlemksv2  36452  cdlemkuv2  36472  cdlemk33N  36514  cdlemk34  36515  cdlemk36  36518  cdlemk19u  36575  cdlemk  36579  tendoex  36580  dvavsca  36622  dvhvscacbv  36704  dvhvscaval  36705  dicopelval  36783  dicelval1sta  36793  diclspsn  36800  dihmeetlem13N  36925  dih1dimatlem0  36934  dih1dimatlem  36935  dihpN  36942  islpolN  37089  hdmap1fval  37403  hdmapfval  37436  ismrc  37581  mzpclval  37605  mzpsubst  37628  mzprename  37629  mzpcompact2lem  37631  eldioph  37638  eldioph2  37642  eldioph2b  37643  eldioph3  37646  rexrabdioph  37675  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  eldioph4i  37693  rabren3dioph  37696  mzpcong  37856  jm2.27dlem1  37893  wepwsolem  37929  aomclem6  37946  aomclem8  37948  dfac11  37949  dgraalem  38032  dgraaub  38035  dgraa0p  38036  mpaaeu  38037  mpaalem  38039  aaitgo  38049  rngunsnply  38060  eliunov2  38288  rfovcnvfvd  38618  fsovfvd  38621  fsovcnvlem  38624  dssmapfv2d  38629  dssmapnvod  38631  clsk1independent  38661  ntrclskb  38684  ntrclsk13  38686  gneispace2  38747  dvconstbi  38850  addrval  38987  subrval  38988  mulvval  38989  fnchoice  39502  refsum2cnlem1  39510  mapsnend  39705  choicefi  39706  axccdom  39730  fmulcl  40131  fmuldfeqlem1  40132  mccllem  40147  mccl  40148  climf  40172  climf2  40216  dvnprodlem1  40479  dvnprodlem3  40481  dvnprod  40482  stoweidlem2  40537  stoweidlem6  40541  stoweidlem8  40543  stoweidlem9  40544  stoweidlem15  40550  stoweidlem16  40551  stoweidlem17  40552  stoweidlem18  40553  stoweidlem21  40556  stoweidlem27  40562  stoweidlem31  40566  stoweidlem36  40571  stoweidlem37  40572  stoweidlem41  40576  stoweidlem43  40578  stoweidlem44  40579  stoweidlem45  40580  stoweidlem46  40581  stoweidlem48  40583  stoweidlem51  40586  stoweidlem55  40590  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  fourierdlem2  40644  fourierdlem3  40645  elaa2lem  40768  etransclem11  40780  etransclem24  40793  etransclem26  40795  etransclem28  40797  etransclem35  40804  rrndistlt  40828  ioorrnopn  40843  subsaliuncllem  40893  sge0val  40901  ismea  40986  caragenval  41028  isome  41029  isomenndlem  41065  hoicvrrex  41091  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  ovnsubadd  41107  hsphoif  41111  hoidmvval  41112  hsphoival  41114  hoidmvlelem3  41132  hoidmvlelem5  41134  hoidmvle  41135  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  ovncvr2  41146  hoidifhspval2  41150  hoiqssbllem2  41158  hspmbllem2  41162  hspmbllem3  41163  hspmbl  41164  ovnovollem1  41191  smfmullem2  41320  smfmul  41323  smfpimcclem  41334  iccpart  41677  iccpartiun  41695  icceuelpart  41697  nnsum3primes4  42001  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbnd  42022  isupwlk  42042  ismgmhm  42108  isrnghm  42217  lincval  42523  lincdifsn  42538  linindslinci  42562  lindslinindsimp1  42571  linds0  42579  el0ldep  42580  lindsrng01  42582  snlindsntorlem  42584  ldepspr  42587  islindeps2  42597  zlmodzxzldep  42618  offval0  42624  bigoval  42668  elbigo  42670  setrecseq  42757  aacllem  42875
  Copyright terms: Public domain W3C validator