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

Theorem fveq1 6087
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 4580 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 5775 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 5798 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5798 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2669 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4578  cio 5752  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798
This theorem is referenced by:  fveq1i  6089  fveq1d  6090  iffv  6100  fvmptdf  6189  fvmptdv2  6191  fsnex  6416  f1prex  6417  isoeq1  6445  oveq  6533  elovmpt3imp  6766  offval  6780  ofrfval  6781  offval3  7031  bropopvvv  7120  bropfvvvvlem  7121  wfrlem1  7279  wfrlem3a  7282  wfrlem15  7294  smoeq  7312  tfrlem12  7350  tz7.44-2  7368  tz7.44-3  7369  rdgeq1  7372  mapsncnv  7768  elixp2  7776  resixpfo  7810  elixpsn  7811  mapsnen  7898  enfixsn  7932  mapxpen  7989  ac6sfi  8067  ordtypelem7  8290  wemaplem1  8312  ixpiunwdom  8357  oemapval  8441  cantnf  8451  wemapwe  8455  cnfcom3clem  8463  infxpenc2lem2  8704  fseqenlem1  8708  dfac8clem  8716  ac5num  8720  acni  8729  acni2  8730  acnlem  8732  dfac4  8806  dfac5lem5  8811  dfac2a  8813  dfac9  8819  dfacacn  8824  dfac12lem1  8826  dfac12r  8829  cofsmo  8952  cfsmolem  8953  cfsmo  8954  cfcoflem  8955  coftr  8956  alephsing  8959  isfin3ds  9012  fin23lem17  9021  fin23lem32  9027  fin23lem39  9033  isf33lem  9049  isf34lem6  9063  axcc2lem  9119  axcc3  9121  axdc2lem  9131  axdc3lem2  9134  axdc3lem3  9135  axdc3  9137  axdc4lem  9138  axcclem  9140  ac6num  9162  axdclem2  9203  konigthlem  9247  inar1  9454  1fv  12285  axdc4uzlem  12602  seqeq3  12626  seqof  12678  ccatfval  13160  wrdl1s1  13196  cshf1  13356  cshweqrep  13367  wrdlen2i  13483  wwlktovf  13496  wwlktovf1  13497  wwlktovfo  13498  wrd2f1tovbij  13500  dfrtrclrec2  13594  rtrclreclem1  13595  rtrclreclem2  13596  rtrclreclem4  13598  dfrtrcl2  13599  clim  14022  rlim  14023  ello1  14043  elo1  14054  summo  14244  fsum  14247  prodmo  14454  fprod  14459  bpolylem  14567  bpolyval  14568  vdwlem6  15477  vdwlem8  15479  ramcl  15520  strfvnd  15659  prdsplusgval  15905  prdsmulrval  15907  prdsleval  15909  prdsdsval  15910  prdsvscaval  15911  xpsff1o  16000  isacs2  16086  isnat  16379  yonedalem3b  16691  yonedainv  16693  ismhm  17109  prdspjmhm  17139  isgrpinv  17244  pwsmulg  17359  isghm  17432  cayleylem2  17605  symgfix2  17608  gsmsymgrfix  17620  gsmsymgreq  17624  symgfixelq  17625  pmtr3ncomlem2  17666  pmtrdifel  17672  pmtrdifwrdel  17677  pmtrdifwrdel2  17678  psgnunilem2  17687  psgnunilem3  17688  efgsdm  17915  efgredlemd  17929  efgredlem  17932  efgred  17933  efgrelexlema  17934  efgrelexlemb  17935  prdsgsum  18149  isabv  18591  islmhm  18797  psrmulfval  19155  evlslem2  19282  evlslem3  19284  evlslem1  19285  mpfrcl  19288  coe1fval  19345  coe1mul2lem2  19408  coe1tm  19413  frgpcyg  19689  psgndiflemB  19713  psgndiflemA  19714  dsmmelbas  19850  frlmipval  19885  frlmphl  19887  uvcf1  19898  islindf  19918  islindf4  19944  madetsumid  20034  mvmulval  20116  marepvval0  20139  mulmarep1gsum2  20147  mdetleib2  20161  m1detdiag  20170  mdetralt  20181  mdetunilem7  20191  mdetunilem9  20193  m2detleiblem3  20202  m2detleiblem4  20203  m2detleib  20204  symgmatr01lem  20226  gsummatr01lem1  20228  gsummatr01lem4  20231  gsummatr01  20232  smadiadetlem3  20241  pmatcoe1fsupp  20273  pmatcollpw3lem  20355  pmatcollpw3fi1lem2  20359  iscnp  20799  1stcfb  21006  ptpjpre1  21132  elpt  21133  elptr  21134  ptpjopn  21173  dfac14  21179  upxp  21184  pthaus  21199  ptrescn  21200  xkoptsub  21215  cnmptkp  21241  xkofvcn  21245  cnmptk1p  21246  cnmptk2  21247  ptunhmeo  21369  ptcmplem3  21616  ptcmplem4  21617  symgtgp  21663  prdstmdd  21685  isucn  21840  imasdsf1olem  21936  prdsxmslem2  22092  tngngp3  22218  nmoval  22277  elcncf  22448  ishtpy  22527  pcoval  22567  om1elbas  22588  elpi1i  22602  iscau  22827  rrxds  22934  mbfi1fseqlem6  23238  mbfi1flimlem  23240  isibl  23283  deg1ldg  23601  deg1leb  23604  elply2  23701  elplyr  23706  ne0p  23712  coeeu  23730  coelem  23731  coeeq  23732  coeidlem  23742  elqaalem3  23825  qaa  23827  iaa  23829  aareccl  23830  aannenlem2  23833  aaliou2  23844  dchrptlem2  24735  dchrpt  24737  dchrsum2  24738  sumdchr2  24740  dchrvmaeq0  24938  rpvmasum2  24946  dchrisum0re  24947  ostth  25073  iscgrg  25153  isismt  25175  israg  25338  iseqlg  25493  brbtwn  25525  brbtwn2  25531  colinearalg  25536  axsegconlem1  25543  axsegcon  25553  ax5seglem5  25559  axpasch  25567  axlowdim  25587  axeuclidlem  25588  axcontlem1  25590  axcontlem2  25591  axcontlem5  25594  wlks  25841  iswlk  25842  wlkcompim  25848  wlkelwrd  25852  iswlkon  25856  istrl  25861  constr1trl  25912  2wlklem1  25921  usg2wlk  25939  iscrct  25946  iscycl  25947  constr3cyclpe  25985  iswwlk  26005  wlkiswwlk2  26019  usg2wlkeq2  26031  wlkiswwlkfun  26039  wlkiswwlksur  26041  wlkiswwlkbij2  26043  wwlknredwwlkn0  26049  wlknwwlknvbij  26062  wwlkextproplem3  26065  wwlkextprop  26066  isclwlk0  26076  isclwwlk  26090  clwwlkprop  26092  clwwlkgt0  26093  clwwlknprop  26094  clwlkisclwwlklem2  26108  clwwlkel  26115  clwwlkf  26116  clwwlkf1  26118  clwwlkvbij  26123  rusgranumwlklem0  26269  rusgranumwlkb0  26274  rusgranumwlks  26277  iseupa  26286  numclwwlkun  26400  numclwwlkovfel2  26404  numclwwlkovgel  26409  extwwlkfab  26411  numclwlk1lem2foa  26412  numclwlk1lem2fv  26414  numclwwlk2lem1  26423  numclwlk2lem2f  26424  numclwlk2lem2f1o  26426  numclwwlk5  26433  numclwwlk7  26435  ex-fv  26486  isnvlem  26643  islno  26786  nmooval  26796  nmblolbi  26833  isphg  26850  ajmoi  26892  ajval  26895  ubthlem3  26906  htthlem  26952  hcau  27219  hlimi  27223  hosmval  27772  hommval  27773  hodmval  27774  hfsmval  27775  hfmmval  27776  adjmo  27869  nmopval  27893  elcnop  27894  ellnop  27895  elunop  27909  elhmop  27910  nmfnval  27913  elcnfn  27919  ellnfn  27920  adjeu  27926  adjval  27927  eigvecval  27933  eigvalfval  27934  adj1  27970  adjeq  27972  hmopadj2  27978  lnopeq0i  28044  lnopeq  28046  elunop2  28050  lnophm  28056  hmopco  28060  nmbdoplb  28062  nmcoplb  28067  lnopcon  28072  lnfn0  28084  lnfnmul  28085  nmbdfnlb  28087  nmcfnlb  28091  lnfncon  28093  riesz4  28101  riesz1  28102  cnlnadjlem9  28112  cnlnadjeu  28115  cnlnssadj  28117  nmopcoi  28132  bra11  28145  cnvbraval  28147  pjss2coi  28201  pjssdif2i  28211  pjssdif1i  28212  pjclem4  28236  pj3si  28244  pj3cor1i  28246  isst  28250  ishst  28251  stri  28294  hstri  28302  aciunf1lem  28638  lmatval  29001  mdetpmtr1  29011  ismeas  29383  isrnmeas  29384  cntnevol  29412  carsgval  29486  sitgval  29515  eulerpartleme  29546  eulerpartlemd  29549  eulerpartlemr  29557  eulerpartlemgvv  29559  eulerpart  29565  cndprobval  29616  signstfvneq0  29769  bnj66  29978  bnj106  29986  bnj125  29990  bnj154  29996  bnj155  29997  bnj526  30006  bnj540  30010  bnj609  30035  bnj611  30036  bnj893  30046  bnj1000  30059  bnj1014  30078  bnj1015  30079  bnj1234  30129  bnj1463  30171  derangenlem  30201  subfacp1lem3  30212  subfacp1lem5  30214  subfacp1lem6  30215  subfacp1  30216  sconpht  30259  cnpcon  30260  txpcon  30262  ptpcon  30263  indispcon  30264  conpcon  30265  cvxpcon  30272  cvmliftmo  30314  cvmliftlem14  30327  cvmliftlem15  30328  cvmliftiota  30331  cvmlift2  30346  cvmliftphtlem  30347  cvmlift3lem2  30350  cvmlift3lem6  30354  cvmlift3lem7  30355  cvmlift3lem9  30357  cvmlift3  30358  mrsubff1  30459  mrsub0  30461  mrsubccat  30463  mrsubcn  30464  elmsubrn  30473  msubrn  30474  msubco  30476  msubvrs  30505  mclsax  30514  shftvalg  30664  poseq  30788  soseq  30789  frrlem1  30818  sltval  30838  nobndlem6  30890  fwddifval  31233  fwddifnval  31234  unceq  32350  matunitlindflem2  32370  poimirlem17  32390  poimirlem20  32393  poimirlem22  32395  poimirlem23  32396  poimirlem27  32400  poimirlem28  32401  poimirlem30  32403  poimirlem31  32404  poimirlem32  32405  poimir  32406  broucube  32407  voliunnfl  32417  volsupnfl  32418  itg2addnclem  32425  itg2addnclem3  32427  itg2addnc  32428  ftc1anclem2  32450  ftc1anclem5  32453  eqfnun  32480  upixp  32488  fdc  32505  isismty  32564  rrnmval  32591  elghomlem2OLD  32649  isrngohom  32728  islfl  33159  isopos  33279  islaut  34181  ispautN  34197  isldil  34208  isltrn  34217  ltrnid  34233  ltrneq2  34246  isdilN  34253  istrnN  34256  trlval  34261  ltrneq3  34307  cdleme50ex  34659  cdleme  34660  cdlemg1a  34670  ltrniotaval  34681  ltrniotavalbN  34684  cdlemeiota  34685  cdlemg2jlemOLDN  34693  cdlemg2fvlem  34694  cdlemg2klem  34695  istendo  34860  tendoplcbv  34875  tendopl  34876  tendoicbv  34893  tendoi  34894  tendoid0  34925  tendo1ne0  34928  cdlemksv2  34947  cdlemkuv2  34967  cdlemk33N  35009  cdlemk34  35010  cdlemk36  35013  cdlemk19u  35070  cdlemk  35074  tendoex  35075  dvavsca  35117  dvhvscacbv  35199  dvhvscaval  35200  dicopelval  35278  dicelval1sta  35288  diclspsn  35295  dihmeetlem13N  35420  dih1dimatlem0  35429  dih1dimatlem  35430  dihpN  35437  islpolN  35584  hdmap1fval  35898  hdmapfval  35931  ismrc  36076  mzpclval  36100  mzpsubst  36123  mzprename  36124  mzpcompact2lem  36126  eldioph  36133  eldioph2  36137  eldioph2b  36138  eldioph3  36141  rexrabdioph  36170  2rexfrabdioph  36172  3rexfrabdioph  36173  4rexfrabdioph  36174  6rexfrabdioph  36175  7rexfrabdioph  36176  eldioph4i  36188  rabren3dioph  36191  mzpcong  36351  jm2.27dlem1  36388  wepwsolem  36424  aomclem6  36441  aomclem8  36443  dfac11  36444  dgraalem  36528  dgraaub  36531  dgraa0p  36532  mpaaeu  36533  mpaalem  36535  aaitgo  36545  rngunsnply  36556  eliunov2  36784  rfovcnvfvd  37115  fsovfvd  37118  fsovcnvlem  37121  dssmapfv2d  37126  dssmapnvod  37128  clsk1independent  37158  ntrclskb  37181  ntrclsk13  37183  gneispace2  37244  dvconstbi  37349  addrval  37485  subrval  37486  mulvval  37487  fnchoice  38005  refsum2cnlem1  38013  mapsnend  38180  choicefi  38181  axccdom  38205  fmulcl  38442  fmuldfeqlem1  38443  mccllem  38458  mccl  38459  climf  38483  climf2  38527  dvnprodlem1  38630  dvnprodlem3  38632  dvnprod  38633  stoweidlem2  38689  stoweidlem6  38693  stoweidlem8  38695  stoweidlem9  38696  stoweidlem15  38702  stoweidlem16  38703  stoweidlem17  38704  stoweidlem18  38705  stoweidlem21  38708  stoweidlem27  38714  stoweidlem31  38718  stoweidlem36  38723  stoweidlem37  38724  stoweidlem41  38728  stoweidlem43  38730  stoweidlem44  38731  stoweidlem45  38732  stoweidlem46  38733  stoweidlem48  38735  stoweidlem51  38738  stoweidlem55  38742  stoweidlem59  38746  stoweidlem60  38747  stoweidlem62  38749  fourierdlem2  38796  fourierdlem3  38797  elaa2lem  38920  etransclem11  38932  etransclem24  38945  etransclem26  38947  etransclem28  38949  etransclem35  38956  rrndistlt  38980  ioorrnopn  38995  subsaliuncllem  39045  sge0val  39053  ismea  39138  caragenval  39177  isome  39178  isomenndlem  39214  hoicvrrex  39240  ovnlecvr  39242  ovncvrrp  39248  ovn0lem  39249  ovnsubaddlem1  39254  ovnsubadd  39256  hsphoif  39260  hoidmvval  39261  hsphoival  39263  hoidmvlelem3  39281  hoidmvlelem5  39283  hoidmvle  39284  ovnhoilem1  39285  ovnhoi  39287  ovnlecvr2  39294  ovncvr2  39295  hoidifhspval2  39299  hoiqssbllem2  39307  hspmbllem2  39311  hspmbllem3  39312  hspmbl  39313  ovnovollem1  39340  smfmullem2  39471  smfmul  39474  iccpart  39749  iccpartiun  39767  icceuelpart  39769  nnsum3primes4  39999  nnsum3primesgbe  40003  nnsum4primesodd  40007  nnsum4primesoddALTV  40008  nnsum4primeseven  40011  nnsum4primesevenALTV  40012  bgoldbtbnd  40020  vtxdgfval  40675  1egrvtxdg1  40717  isewlk  40796  is1wlk  40805  isWlk  40806  uspgr2wlkeq2  40847  iswlkOn  40857  isclWlk  40971  isCrct  40988  isCycl  40989  iswwlks  41031  wwlknon  41045  1wlkiswwlks2  41064  wlkwwlkfun  41084  wlkwwlksur  41086  wlkwwlkbij2  41088  wwlksnredwwlkn0  41094  wlksnwwlknvbij  41106  wwlksnextproplem3  41109  wwlksnextprop  41110  umgr2wlk  41148  wwlks2onv  41150  elwwlks2  41162  elwspths2spth  41163  rusgrnumwwlkb0  41166  rusgrnumwwlks  41169  isclwwlks  41180  clwlkclwwlklem1  41200  clwwlksel  41213  clwwlksf  41214  clwwlksf1  41216  clwwlksvbij  41221  clwwlksnun  41273  uhgr3cyclex  41341  fusgr2wsp2nb  41490  fusgreg2wsp  41492  2wspmdisj  41493  fusgreghash2wsp  41494  av-numclwwlkovfel2  41506  av-numclwwlkovgel  41511  av-extwwlkfab  41512  av-numclwlk1lem2foa  41513  av-numclwlk1lem2fv  41515  av-numclwwlk2lem1  41524  av-numclwlk2lem2f  41525  av-numclwlk2lem2f1o  41527  av-numclwwlk5  41534  av-numclwwlk6  41536  ismgmhm  41565  isrnghm  41674  lincval  41984  lincdifsn  41999  linindslinci  42023  lindslinindsimp1  42032  linds0  42040  el0ldep  42041  lindsrng01  42043  snlindsntorlem  42045  ldepspr  42048  islindeps2  42058  zlmodzxzldep  42079  offval0  42085  bigoval  42133  elbigo  42135  aacllem  42309
  Copyright terms: Public domain W3C validator