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

Theorem fveq1 6343
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 4798 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 6025 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 6049 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 6049 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2811 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624   class class class wbr 4796  cio 6002  cfv 6041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049
This theorem is referenced by:  fveq1i  6345  fveq1d  6346  iffv  6358  fvmptd3f  6449  fvmptdv2  6452  fsnex  6693  f1prex  6694  isoeq1  6722  oveq  6811  elovmpt3imp  7047  offval  7061  ofrfval  7062  offval3  7319  bropopvvv  7415  bropfvvvvlem  7416  wfrlem1  7575  wfrlem3a  7578  wfrlem15  7590  smoeq  7608  tfrlem12  7646  tz7.44-2  7664  tz7.44-3  7665  rdgeq1  7668  mapsncnv  8062  elixp2  8070  resixpfo  8104  elixpsn  8105  mapsnen  8192  enfixsn  8226  mapxpen  8283  ac6sfi  8361  ordtypelem7  8586  wemaplem1  8608  ixpiunwdom  8653  oemapval  8745  cantnf  8755  wemapwe  8759  cnfcom3clem  8767  infxpenc2lem2  9025  fseqenlem1  9029  dfac8clem  9037  ac5num  9041  acni  9050  acni2  9051  acnlem  9053  dfac4  9127  dfac5lem5  9132  dfac2a  9134  dfac9  9142  dfacacn  9147  dfac12lem1  9149  dfac12r  9152  cofsmo  9275  cfsmolem  9276  cfsmo  9277  cfcoflem  9278  coftr  9279  alephsing  9282  isfin3ds  9335  fin23lem17  9344  fin23lem32  9350  fin23lem39  9356  isf33lem  9372  isf34lem6  9386  axcc2lem  9442  axcc3  9444  axdc2lem  9454  axdc3lem2  9457  axdc3lem3  9458  axdc3  9460  axdc4lem  9461  axcclem  9463  ac6num  9485  axdclem2  9526  konigthlem  9574  inar1  9781  1fv  12644  axdc4uzlem  12968  seqeq3  12992  seqof  13044  ccatfval  13537  wrdl1s1  13577  ccat1st1st  13594  cshf1  13748  cshweqrep  13759  wrdlen2i  13879  wwlktovf  13892  wwlktovf1  13893  wwlktovfo  13894  wrd2f1tovbij  13896  dfrtrclrec2  13988  rtrclreclem1  13989  rtrclreclem2  13990  rtrclreclem4  13992  dfrtrcl2  13993  clim  14416  rlim  14417  ello1  14437  elo1  14448  summo  14639  fsum  14642  prodmo  14857  fprod  14862  bpolylem  14970  bpolyval  14971  vdwlem6  15884  vdwlem8  15886  ramcl  15927  strfvnd  16070  prdsplusgval  16327  prdsmulrval  16329  prdsleval  16331  prdsdsval  16332  prdsvscaval  16333  xpsff1o  16422  isacs2  16507  isnat  16800  yonedalem3b  17112  yonedainv  17114  ismhm  17530  prdspjmhm  17560  isgrpinv  17665  pwsmulg  17780  isghm  17853  cayleylem2  18025  symgfix2  18028  gsmsymgrfix  18040  gsmsymgreq  18044  symgfixelq  18045  pmtr3ncomlem2  18086  pmtrdifel  18092  pmtrdifwrdel  18097  pmtrdifwrdel2  18098  psgnunilem2  18107  psgnunilem3  18108  efgsdm  18335  efgredlemd  18349  efgredlem  18352  efgred  18353  efgrelexlema  18354  efgrelexlemb  18355  prdsgsum  18569  isabv  19013  islmhm  19221  psrmulfval  19579  evlslem2  19706  evlslem3  19708  evlslem1  19709  mpfrcl  19712  coe1fval  19769  coe1mul2lem2  19832  coe1tm  19837  frgpcyg  20116  psgndiflemB  20140  psgndiflemA  20141  dsmmelbas  20277  frlmipval  20312  frlmphl  20314  uvcf1  20325  islindf  20345  islindf4  20371  madetsumid  20461  mvmulval  20543  marepvval0  20566  mulmarep1gsum2  20574  mdetleib2  20588  m1detdiag  20597  mdetralt  20608  mdetunilem7  20618  mdetunilem9  20620  m2detleiblem3  20629  m2detleiblem4  20630  m2detleib  20631  symgmatr01lem  20653  gsummatr01lem1  20655  gsummatr01lem4  20658  gsummatr01  20659  smadiadetlem3  20668  pmatcoe1fsupp  20700  pmatcollpw3lem  20782  pmatcollpw3fi1lem2  20786  iscnp  21235  1stcfb  21442  ptpjpre1  21568  elpt  21569  elptr  21570  ptpjopn  21609  dfac14  21615  upxp  21620  pthaus  21635  ptrescn  21636  xkoptsub  21651  cnmptkp  21677  xkofvcn  21681  cnmptk1p  21682  cnmptk2  21683  ptunhmeo  21805  ptcmplem3  22051  ptcmplem4  22052  symgtgp  22098  prdstmdd  22120  isucn  22275  imasdsf1olem  22371  prdsxmslem2  22527  tngngp3  22653  nmoval  22712  elcncf  22885  ishtpy  22964  pcoval  23003  om1elbas  23024  elpi1i  23038  iscau  23266  rrxds  23373  mbfi1fseqlem6  23678  mbfi1flimlem  23680  isibl  23723  deg1ldg  24043  deg1leb  24046  elply2  24143  elplyr  24148  ne0p  24154  coeeu  24172  coelem  24173  coeeq  24174  coeidlem  24184  elqaalem3  24267  qaa  24269  iaa  24271  aareccl  24272  aannenlem2  24275  aaliou2  24286  dchrptlem2  25181  dchrpt  25183  dchrsum2  25184  sumdchr2  25186  dchrvmaeq0  25384  rpvmasum2  25392  dchrisum0re  25393  ostth  25519  iscgrg  25598  isismt  25620  israg  25783  iseqlg  25938  brbtwn  25970  brbtwn2  25976  colinearalg  25981  axsegconlem1  25988  axsegcon  25998  ax5seglem5  26004  axpasch  26012  axlowdim  26032  axeuclidlem  26033  axcontlem1  26035  axcontlem2  26036  axcontlem5  26039  vtxdgfval  26565  1egrvtxdg1  26607  isewlk  26700  iswlk  26708  uspgr2wlkeq2  26745  iswlkon  26755  isclwlk  26871  iscrct  26888  iscycl  26889  iswwlks  26931  wwlknon  26955  wwlknonOLD  26957  wlkiswwlks2  26976  wlkwwlkfun  26996  wlkwwlksur  26998  wlkwwlkbij2  27000  wwlksnredwwlkn0  27006  wlksnwwlknvbij  27018  wwlksnextproplem3  27021  wwlksnextprop  27022  umgr2wlk  27061  midwwlks2s3  27064  elwwlks2  27080  elwspths2spth  27081  rusgrnumwwlkslem  27083  rusgrnumwwlkb0  27085  rusgrnumwwlks  27088  isclwwlk  27099  clwlkclwwlklem1  27114  clwwlkn1loopb  27164  clwwlkel  27167  clwwlkf  27168  clwwlkf1  27170  isclwwlknon  27229  isclwwlknonOLD  27230  clwwlknon1  27237  s2elclwwlknon2  27244  clwwlkvbij  27254  clwwlkvbijOLD  27255  clwwlknunOLD  27257  uhgr3cyclex  27326  fusgreg2wsplem  27479  fusgr2wsp2nb  27480  fusgreghash2wsp  27484  2clwwlkel  27498  numclwwlkovgelOLD  27501  extwwlkfabel  27504  numclwlk1lem2fv  27507  numclwwlk1lem2  27511  clwwlknonclwlknonf1o  27514  dlwwlknondlwlknonf1o  27518  numclwwlk2lem1  27529  numclwlk2lem2f  27530  numclwlk2lem2f1o  27532  numclwwlk2lem1OLD  27536  numclwlk2lem2fOLD  27537  numclwlk2lem2f1oOLD  27539  ex-fv  27603  isnvlem  27766  islno  27909  nmooval  27919  nmblolbi  27956  isphg  27973  ajmoi  28015  ajval  28018  ubthlem3  28029  htthlem  28075  hcau  28342  hlimi  28346  hosmval  28895  hommval  28896  hodmval  28897  hfsmval  28898  hfmmval  28899  adjmo  28992  nmopval  29016  elcnop  29017  ellnop  29018  elunop  29032  elhmop  29033  nmfnval  29036  elcnfn  29042  ellnfn  29043  adjeu  29049  adjval  29050  eigvecval  29056  eigvalfval  29057  adj1  29093  adjeq  29095  hmopadj2  29101  lnopeq0i  29167  lnopeq  29169  elunop2  29173  lnophm  29179  hmopco  29183  nmbdoplb  29185  nmcoplb  29190  lnopcon  29195  lnfn0  29207  lnfnmul  29208  nmbdfnlb  29210  nmcfnlb  29214  lnfncon  29216  riesz4  29224  riesz1  29225  cnlnadjlem9  29235  cnlnadjeu  29238  cnlnssadj  29240  nmopcoi  29255  bra11  29268  cnvbraval  29270  pjss2coi  29324  pjssdif2i  29334  pjssdif1i  29335  pjclem4  29359  pj3si  29367  pj3cor1i  29369  isst  29373  ishst  29374  stri  29417  hstri  29425  aciunf1lem  29763  lmatval  30180  mdetpmtr1  30190  ismeas  30563  isrnmeas  30564  cntnevol  30592  carsgval  30666  sitgval  30695  eulerpartleme  30726  eulerpartlemd  30729  eulerpartlemr  30737  eulerpartlemgvv  30739  eulerpart  30745  cndprobval  30796  signstfvneq0  30950  reprsum  30992  reprsuc  30994  reprpmtf1o  31005  reprdifc  31006  breprexp  31012  vtsval  31016  hgt750lemb  31035  hgt750lema  31036  hgt750leme  31037  bnj66  31229  bnj106  31237  bnj125  31241  bnj154  31247  bnj155  31248  bnj526  31257  bnj540  31261  bnj609  31286  bnj611  31287  bnj893  31297  bnj1000  31310  bnj1014  31329  bnj1015  31330  bnj1234  31380  bnj1463  31422  derangenlem  31452  subfacp1lem3  31463  subfacp1lem5  31465  subfacp1lem6  31466  subfacp1  31467  sconnpht  31510  cnpconn  31511  txpconn  31513  ptpconn  31514  indispconn  31515  connpconn  31516  cvxpconn  31523  cvmliftmo  31565  cvmliftlem14  31578  cvmliftlem15  31579  cvmliftiota  31582  cvmlift2  31597  cvmliftphtlem  31598  cvmlift3lem2  31601  cvmlift3lem6  31605  cvmlift3lem7  31606  cvmlift3lem9  31608  cvmlift3  31609  mrsubff1  31710  mrsub0  31712  mrsubccat  31714  mrsubcn  31715  elmsubrn  31724  msubrn  31725  msubco  31727  msubvrs  31756  mclsax  31765  shftvalg  31916  poseq  32051  soseq  32052  frrlem1  32078  sltval  32098  nolesgn2o  32122  noresle  32144  noprefixmo  32146  nosupfv  32150  fwddifval  32567  fwddifnval  32568  bj-evalval  33325  unceq  33691  matunitlindflem2  33711  poimirlem17  33731  poimirlem20  33734  poimirlem22  33736  poimirlem23  33737  poimirlem27  33741  poimirlem28  33742  poimirlem30  33744  poimirlem31  33745  poimirlem32  33746  poimir  33747  broucube  33748  voliunnfl  33758  volsupnfl  33759  itg2addnclem  33766  itg2addnclem3  33768  itg2addnc  33769  ftc1anclem2  33791  ftc1anclem5  33794  eqfnun  33821  upixp  33829  fdc  33846  isismty  33905  rrnmval  33932  elghomlem2OLD  33990  isrngohom  34069  islfl  34842  isopos  34962  islaut  35864  ispautN  35880  isldil  35891  isltrn  35900  ltrnid  35916  ltrneq2  35929  isdilN  35936  istrnN  35939  trlval  35944  ltrneq3  35990  cdleme50ex  36341  cdleme  36342  cdlemg1a  36352  ltrniotaval  36363  ltrniotavalbN  36366  cdlemeiota  36367  cdlemg2jlemOLDN  36375  cdlemg2fvlem  36376  cdlemg2klem  36377  istendo  36542  tendoplcbv  36557  tendopl  36558  tendoicbv  36575  tendoi  36576  tendoid0  36607  tendo1ne0  36610  cdlemksv2  36629  cdlemkuv2  36649  cdlemk33N  36691  cdlemk34  36692  cdlemk36  36695  cdlemk19u  36752  cdlemk  36756  tendoex  36757  dvavsca  36799  dvhvscacbv  36881  dvhvscaval  36882  dicopelval  36960  dicelval1sta  36970  diclspsn  36977  dihmeetlem13N  37102  dih1dimatlem0  37111  dih1dimatlem  37112  dihpN  37119  islpolN  37266  hdmap1fval  37580  hdmapfval  37613  ismrc  37758  mzpclval  37782  mzpsubst  37805  mzprename  37806  mzpcompact2lem  37808  eldioph  37815  eldioph2  37819  eldioph2b  37820  eldioph3  37823  rexrabdioph  37852  2rexfrabdioph  37854  3rexfrabdioph  37855  4rexfrabdioph  37856  6rexfrabdioph  37857  7rexfrabdioph  37858  eldioph4i  37870  rabren3dioph  37873  mzpcong  38033  jm2.27dlem1  38070  wepwsolem  38106  aomclem6  38123  aomclem8  38125  dfac11  38126  dgraalem  38209  dgraaub  38212  dgraa0p  38213  mpaaeu  38214  mpaalem  38216  aaitgo  38226  rngunsnply  38237  eliunov2  38465  rfovcnvfvd  38795  fsovfvd  38798  fsovcnvlem  38801  dssmapfv2d  38806  dssmapnvod  38808  clsk1independent  38838  ntrclskb  38861  ntrclsk13  38863  gneispace2  38924  dvconstbi  39027  addrval  39164  subrval  39165  mulvval  39166  fnchoice  39679  refsum2cnlem1  39687  mapsnend  39882  choicefi  39883  axccdom  39907  fmulcl  40308  fmuldfeqlem1  40309  mccllem  40324  mccl  40325  climf  40349  climf2  40393  dvnprodlem1  40656  dvnprodlem3  40658  dvnprod  40659  stoweidlem2  40714  stoweidlem6  40718  stoweidlem8  40720  stoweidlem9  40721  stoweidlem15  40727  stoweidlem16  40728  stoweidlem17  40729  stoweidlem18  40730  stoweidlem21  40733  stoweidlem27  40739  stoweidlem31  40743  stoweidlem36  40748  stoweidlem37  40749  stoweidlem41  40753  stoweidlem43  40755  stoweidlem44  40756  stoweidlem45  40757  stoweidlem46  40758  stoweidlem48  40760  stoweidlem51  40763  stoweidlem55  40767  stoweidlem59  40771  stoweidlem60  40772  stoweidlem62  40774  fourierdlem2  40821  fourierdlem3  40822  elaa2lem  40945  etransclem11  40957  etransclem24  40970  etransclem26  40972  etransclem28  40974  etransclem35  40981  rrndistlt  41005  ioorrnopn  41020  subsaliuncllem  41070  sge0val  41078  ismea  41163  caragenval  41205  isome  41206  isomenndlem  41242  hoicvrrex  41268  ovnlecvr  41270  ovncvrrp  41276  ovn0lem  41277  ovnsubaddlem1  41282  ovnsubadd  41284  hsphoif  41288  hoidmvval  41289  hsphoival  41291  hoidmvlelem3  41309  hoidmvlelem5  41311  hoidmvle  41312  ovnhoilem1  41313  ovnhoi  41315  ovnlecvr2  41322  ovncvr2  41323  hoidifhspval2  41327  hoiqssbllem2  41335  hspmbllem2  41339  hspmbllem3  41340  hspmbl  41341  ovnovollem1  41368  smfmullem2  41497  smfmul  41500  smfpimcclem  41511  iccpart  41854  iccpartiun  41872  icceuelpart  41874  nnsum3primes4  42178  nnsum3primesgbe  42182  nnsum4primesodd  42186  nnsum4primesoddALTV  42187  nnsum4primeseven  42190  nnsum4primesevenALTV  42191  bgoldbtbnd  42199  isupwlk  42219  ismgmhm  42285  isrnghm  42394  lincval  42700  lincdifsn  42715  linindslinci  42739  lindslinindsimp1  42748  linds0  42756  el0ldep  42757  lindsrng01  42759  snlindsntorlem  42761  ldepspr  42764  islindeps2  42774  zlmodzxzldep  42795  offval0  42801  bigoval  42845  elbigo  42847  setrecseq  42934  aacllem  43052
  Copyright terms: Public domain W3C validator