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

Theorem fveq1 6102
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 4585 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 5789 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 5812 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5812 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2669 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4583  cio 5766  cfv 5804
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 4373  df-br 4584  df-iota 5768  df-fv 5812
This theorem is referenced by:  fveq1i  6104  fveq1d  6105  iffv  6115  fvmptdf  6204  fvmptdv2  6206  fsnex  6438  f1prex  6439  isoeq1  6467  oveq  6555  elovmpt3imp  6788  offval  6802  ofrfval  6803  offval3  7053  bropopvvv  7142  bropfvvvvlem  7143  wfrlem1  7301  wfrlem3a  7304  wfrlem15  7316  smoeq  7334  tfrlem12  7372  tz7.44-2  7390  tz7.44-3  7391  rdgeq1  7394  mapsncnv  7790  elixp2  7798  resixpfo  7832  elixpsn  7833  mapsnen  7920  enfixsn  7954  mapxpen  8011  ac6sfi  8089  ordtypelem7  8312  wemaplem1  8334  ixpiunwdom  8379  oemapval  8463  cantnf  8473  wemapwe  8477  cnfcom3clem  8485  infxpenc2lem2  8726  fseqenlem1  8730  dfac8clem  8738  ac5num  8742  acni  8751  acni2  8752  acnlem  8754  dfac4  8828  dfac5lem5  8833  dfac2a  8835  dfac9  8841  dfacacn  8846  dfac12lem1  8848  dfac12r  8851  cofsmo  8974  cfsmolem  8975  cfsmo  8976  cfcoflem  8977  coftr  8978  alephsing  8981  isfin3ds  9034  fin23lem17  9043  fin23lem32  9049  fin23lem39  9055  isf33lem  9071  isf34lem6  9085  axcc2lem  9141  axcc3  9143  axdc2lem  9153  axdc3lem2  9156  axdc3lem3  9157  axdc3  9159  axdc4lem  9160  axcclem  9162  ac6num  9184  axdclem2  9225  konigthlem  9269  inar1  9476  1fv  12327  axdc4uzlem  12644  seqeq3  12668  seqof  12720  ccatfval  13211  wrdl1s1  13247  cshf1  13407  cshweqrep  13418  wrdlen2i  13534  wwlktovf  13547  wwlktovf1  13548  wwlktovfo  13549  wrd2f1tovbij  13551  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649  dfrtrcl2  13650  clim  14073  rlim  14074  ello1  14094  elo1  14105  summo  14295  fsum  14298  prodmo  14505  fprod  14510  bpolylem  14618  bpolyval  14619  vdwlem6  15528  vdwlem8  15530  ramcl  15571  strfvnd  15710  prdsplusgval  15956  prdsmulrval  15958  prdsleval  15960  prdsdsval  15961  prdsvscaval  15962  xpsff1o  16051  isacs2  16137  isnat  16430  yonedalem3b  16742  yonedainv  16744  ismhm  17160  prdspjmhm  17190  isgrpinv  17295  pwsmulg  17410  isghm  17483  cayleylem2  17656  symgfix2  17659  gsmsymgrfix  17671  gsmsymgreq  17675  symgfixelq  17676  pmtr3ncomlem2  17717  pmtrdifel  17723  pmtrdifwrdel  17728  pmtrdifwrdel2  17729  psgnunilem2  17738  psgnunilem3  17739  efgsdm  17966  efgredlemd  17980  efgredlem  17983  efgred  17984  efgrelexlema  17985  efgrelexlemb  17986  prdsgsum  18200  isabv  18642  islmhm  18848  psrmulfval  19206  evlslem2  19333  evlslem3  19335  evlslem1  19336  mpfrcl  19339  coe1fval  19396  coe1mul2lem2  19459  coe1tm  19464  frgpcyg  19741  psgndiflemB  19765  psgndiflemA  19766  dsmmelbas  19902  frlmipval  19937  frlmphl  19939  uvcf1  19950  islindf  19970  islindf4  19996  madetsumid  20086  mvmulval  20168  marepvval0  20191  mulmarep1gsum2  20199  mdetleib2  20213  m1detdiag  20222  mdetralt  20233  mdetunilem7  20243  mdetunilem9  20245  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  symgmatr01lem  20278  gsummatr01lem1  20280  gsummatr01lem4  20283  gsummatr01  20284  smadiadetlem3  20293  pmatcoe1fsupp  20325  pmatcollpw3lem  20407  pmatcollpw3fi1lem2  20411  iscnp  20851  1stcfb  21058  ptpjpre1  21184  elpt  21185  elptr  21186  ptpjopn  21225  dfac14  21231  upxp  21236  pthaus  21251  ptrescn  21252  xkoptsub  21267  cnmptkp  21293  xkofvcn  21297  cnmptk1p  21298  cnmptk2  21299  ptunhmeo  21421  ptcmplem3  21668  ptcmplem4  21669  symgtgp  21715  prdstmdd  21737  isucn  21892  imasdsf1olem  21988  prdsxmslem2  22144  tngngp3  22270  nmoval  22329  elcncf  22500  ishtpy  22579  pcoval  22619  om1elbas  22640  elpi1i  22654  iscau  22882  rrxds  22989  mbfi1fseqlem6  23293  mbfi1flimlem  23295  isibl  23338  deg1ldg  23656  deg1leb  23659  elply2  23756  elplyr  23761  ne0p  23767  coeeu  23785  coelem  23786  coeeq  23787  coeidlem  23797  elqaalem3  23880  qaa  23882  iaa  23884  aareccl  23885  aannenlem2  23888  aaliou2  23899  dchrptlem2  24790  dchrpt  24792  dchrsum2  24793  sumdchr2  24795  dchrvmaeq0  24993  rpvmasum2  25001  dchrisum0re  25002  ostth  25128  iscgrg  25207  isismt  25229  israg  25392  iseqlg  25547  brbtwn  25579  brbtwn2  25585  colinearalg  25590  axsegconlem1  25597  axsegcon  25607  ax5seglem5  25613  axpasch  25621  axlowdim  25641  axeuclidlem  25642  axcontlem1  25644  axcontlem2  25645  axcontlem5  25648  wlks  26047  iswlk  26048  wlkcompim  26054  wlkelwrd  26058  iswlkon  26062  istrl  26067  constr1trl  26118  2wlklem1  26127  usg2wlk  26145  iscrct  26152  iscycl  26153  constr3cyclpe  26191  iswwlk  26211  wlkiswwlk2  26225  usg2wlkeq2  26237  wlkiswwlkfun  26245  wlkiswwlksur  26247  wlkiswwlkbij2  26249  wwlknredwwlkn0  26255  wlknwwlknvbij  26268  wwlkextproplem3  26271  wwlkextprop  26272  isclwlk0  26282  isclwwlk  26296  clwwlkprop  26298  clwwlkgt0  26299  clwwlknprop  26300  clwlkisclwwlklem2  26314  clwwlkel  26321  clwwlkf  26322  clwwlkf1  26324  clwwlkvbij  26329  rusgranumwlklem0  26475  rusgranumwlkb0  26480  rusgranumwlks  26483  iseupa  26492  numclwwlkun  26606  numclwwlkovfel2  26610  numclwwlkovgel  26615  extwwlkfab  26617  numclwlk1lem2foa  26618  numclwlk1lem2fv  26620  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  numclwwlk5  26639  numclwwlk7  26641  ex-fv  26692  isnvlem  26849  islno  26992  nmooval  27002  nmblolbi  27039  isphg  27056  ajmoi  27098  ajval  27101  ubthlem3  27112  htthlem  27158  hcau  27425  hlimi  27429  hosmval  27978  hommval  27979  hodmval  27980  hfsmval  27981  hfmmval  27982  adjmo  28075  nmopval  28099  elcnop  28100  ellnop  28101  elunop  28115  elhmop  28116  nmfnval  28119  elcnfn  28125  ellnfn  28126  adjeu  28132  adjval  28133  eigvecval  28139  eigvalfval  28140  adj1  28176  adjeq  28178  hmopadj2  28184  lnopeq0i  28250  lnopeq  28252  elunop2  28256  lnophm  28262  hmopco  28266  nmbdoplb  28268  nmcoplb  28273  lnopcon  28278  lnfn0  28290  lnfnmul  28291  nmbdfnlb  28293  nmcfnlb  28297  lnfncon  28299  riesz4  28307  riesz1  28308  cnlnadjlem9  28318  cnlnadjeu  28321  cnlnssadj  28323  nmopcoi  28338  bra11  28351  cnvbraval  28353  pjss2coi  28407  pjssdif2i  28417  pjssdif1i  28418  pjclem4  28442  pj3si  28450  pj3cor1i  28452  isst  28456  ishst  28457  stri  28500  hstri  28508  aciunf1lem  28844  lmatval  29207  mdetpmtr1  29217  ismeas  29589  isrnmeas  29590  cntnevol  29618  carsgval  29692  sitgval  29721  eulerpartleme  29752  eulerpartlemd  29755  eulerpartlemr  29763  eulerpartlemgvv  29765  eulerpart  29771  cndprobval  29822  signstfvneq0  29975  bnj66  30184  bnj106  30192  bnj125  30196  bnj154  30202  bnj155  30203  bnj526  30212  bnj540  30216  bnj609  30241  bnj611  30242  bnj893  30252  bnj1000  30265  bnj1014  30284  bnj1015  30285  bnj1234  30335  bnj1463  30377  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  subfacp1  30422  sconpht  30465  cnpcon  30466  txpcon  30468  ptpcon  30469  indispcon  30470  conpcon  30471  cvxpcon  30478  cvmliftmo  30520  cvmliftlem14  30533  cvmliftlem15  30534  cvmliftiota  30537  cvmlift2  30552  cvmliftphtlem  30553  cvmlift3lem2  30556  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem9  30563  cvmlift3  30564  mrsubff1  30665  mrsub0  30667  mrsubccat  30669  mrsubcn  30670  elmsubrn  30679  msubrn  30680  msubco  30682  msubvrs  30711  mclsax  30720  shftvalg  30870  poseq  30994  soseq  30995  frrlem1  31024  sltval  31044  nobndlem6  31096  fwddifval  31439  fwddifnval  31440  unceq  32556  matunitlindflem2  32576  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem27  32606  poimirlem28  32607  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  broucube  32613  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem2  32656  ftc1anclem5  32659  eqfnun  32686  upixp  32694  fdc  32711  isismty  32770  rrnmval  32797  elghomlem2OLD  32855  isrngohom  32934  islfl  33365  isopos  33485  islaut  34387  ispautN  34403  isldil  34414  isltrn  34423  ltrnid  34439  ltrneq2  34452  isdilN  34459  istrnN  34462  trlval  34467  ltrneq3  34513  cdleme50ex  34865  cdleme  34866  cdlemg1a  34876  ltrniotaval  34887  ltrniotavalbN  34890  cdlemeiota  34891  cdlemg2jlemOLDN  34899  cdlemg2fvlem  34900  cdlemg2klem  34901  istendo  35066  tendoplcbv  35081  tendopl  35082  tendoicbv  35099  tendoi  35100  tendoid0  35131  tendo1ne0  35134  cdlemksv2  35153  cdlemkuv2  35173  cdlemk33N  35215  cdlemk34  35216  cdlemk36  35219  cdlemk19u  35276  cdlemk  35280  tendoex  35281  dvavsca  35323  dvhvscacbv  35405  dvhvscaval  35406  dicopelval  35484  dicelval1sta  35494  diclspsn  35501  dihmeetlem13N  35626  dih1dimatlem0  35635  dih1dimatlem  35636  dihpN  35643  islpolN  35790  hdmap1fval  36104  hdmapfval  36137  ismrc  36282  mzpclval  36306  mzpsubst  36329  mzprename  36330  mzpcompact2lem  36332  eldioph  36339  eldioph2  36343  eldioph2b  36344  eldioph3  36347  rexrabdioph  36376  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  eldioph4i  36394  rabren3dioph  36397  mzpcong  36557  jm2.27dlem1  36594  wepwsolem  36630  aomclem6  36647  aomclem8  36649  dfac11  36650  dgraalem  36734  dgraaub  36737  dgraa0p  36738  mpaaeu  36739  mpaalem  36741  aaitgo  36751  rngunsnply  36762  eliunov2  36990  rfovcnvfvd  37321  fsovfvd  37324  fsovcnvlem  37327  dssmapfv2d  37332  dssmapnvod  37334  clsk1independent  37364  ntrclskb  37387  ntrclsk13  37389  gneispace2  37450  dvconstbi  37555  addrval  37691  subrval  37692  mulvval  37693  fnchoice  38211  refsum2cnlem1  38219  mapsnend  38386  choicefi  38387  axccdom  38411  fmulcl  38648  fmuldfeqlem1  38649  mccllem  38664  mccl  38665  climf  38689  climf2  38733  dvnprodlem1  38836  dvnprodlem3  38838  dvnprod  38839  stoweidlem2  38895  stoweidlem6  38899  stoweidlem8  38901  stoweidlem9  38902  stoweidlem15  38908  stoweidlem16  38909  stoweidlem17  38910  stoweidlem18  38911  stoweidlem21  38914  stoweidlem27  38920  stoweidlem31  38924  stoweidlem36  38929  stoweidlem37  38930  stoweidlem41  38934  stoweidlem43  38936  stoweidlem44  38937  stoweidlem45  38938  stoweidlem46  38939  stoweidlem48  38941  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  fourierdlem2  39002  fourierdlem3  39003  elaa2lem  39126  etransclem11  39138  etransclem24  39151  etransclem26  39153  etransclem28  39155  etransclem35  39162  rrndistlt  39186  ioorrnopn  39201  subsaliuncllem  39251  sge0val  39259  ismea  39344  caragenval  39383  isome  39384  isomenndlem  39420  hoicvrrex  39446  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  ovnsubadd  39462  hsphoif  39466  hoidmvval  39467  hsphoival  39469  hoidmvlelem3  39487  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  ovncvr2  39501  hoidifhspval2  39505  hoiqssbllem2  39513  hspmbllem2  39517  hspmbllem3  39518  hspmbl  39519  ovnovollem1  39546  smfmullem2  39677  smfmul  39680  iccpart  39954  iccpartiun  39972  icceuelpart  39974  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbnd  40225  vtxdgfval  40683  1egrvtxdg1  40725  isewlk  40804  is1wlk  40813  isWlk  40814  uspgr2wlkeq2  40855  iswlkOn  40865  isclWlk  40979  isCrct  40996  isCycl  40997  iswwlks  41039  wwlknon  41053  1wlkiswwlks2  41072  wlkwwlkfun  41092  wlkwwlksur  41094  wlkwwlkbij2  41096  wwlksnredwwlkn0  41102  wlksnwwlknvbij  41114  wwlksnextproplem3  41117  wwlksnextprop  41118  umgr2wlk  41156  wwlks2onv  41158  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlkb0  41174  rusgrnumwwlks  41177  isclwwlks  41188  clwlkclwwlklem1  41208  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  clwwlksvbij  41229  clwwlksnun  41281  uhgr3cyclex  41349  fusgr2wsp2nb  41498  fusgreg2wsp  41500  2wspmdisj  41501  fusgreghash2wsp  41502  av-numclwwlkovfel2  41514  av-numclwwlkovgel  41519  av-extwwlkfab  41520  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fv  41523  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-numclwwlk5  41542  av-numclwwlk6  41544  ismgmhm  41573  isrnghm  41682  lincval  41992  lincdifsn  42007  linindslinci  42031  lindslinindsimp1  42040  linds0  42048  el0ldep  42049  lindsrng01  42051  snlindsntorlem  42053  ldepspr  42056  islindeps2  42066  zlmodzxzldep  42087  offval0  42093  bigoval  42141  elbigo  42143  setrecseq  42231  aacllem  42356
  Copyright terms: Public domain W3C validator