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

Theorem fveq1 6651
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 5044 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 6318 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 6342 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 6342 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2882 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538   class class class wbr 5042  cio 6291  cfv 6334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342
This theorem is referenced by:  fveq1i  6653  fveq1d  6654  iffv  6669  fvmptd3f  6765  fvmptdv2  6768  fsnex  7022  f1prex  7023  isoeq1  7054  oveq  7146  elovmpt3imp  7387  offval  7401  ofrfval  7402  offval3  7669  bropopvvv  7772  bropfvvvvlem  7773  wfrlem1  7941  wfrlem3a  7944  wfrlem15  7956  smoeq  7974  tfrlem12  8012  tz7.44-2  8030  tz7.44-3  8031  rdgeq1  8034  mapsncnv  8444  elixp2  8452  resixpfo  8487  elixpsn  8488  mapsnend  8575  enfixsn  8613  mapxpen  8671  ac6sfi  8750  ordtypelem7  8976  wemaplem1  8998  ixpiunwdom  9042  oemapval  9134  cantnf  9144  wemapwe  9148  cnfcom3clem  9156  updjud  9351  infxpenc2lem2  9435  fseqenlem1  9439  dfac8clem  9447  ac5num  9451  acni  9460  acni2  9461  acnlem  9463  dfac4  9537  dfac5lem5  9542  dfac2a  9544  dfac9  9551  dfacacn  9556  dfac12lem1  9558  dfac12r  9561  cofsmo  9680  cfsmolem  9681  cfsmo  9682  cfcoflem  9683  coftr  9684  alephsing  9687  isfin3ds  9740  fin23lem17  9749  fin23lem32  9755  fin23lem39  9761  isf33lem  9777  isf34lem6  9791  axcc2lem  9847  axcc3  9849  axdc2lem  9859  axdc3lem2  9862  axdc3lem3  9863  axdc3  9865  axdc4lem  9866  axcclem  9868  ac6num  9890  axdclem2  9931  konigthlem  9979  inar1  10186  1fv  13021  axdc4uzlem  13346  seqeq3  13369  seqof  13423  ccatfval  13916  wrdl1s1  13959  ccat1st1st  13975  cshf1  14163  cshweqrep  14174  wrdlen2i  14295  wwlktovf  14311  wwlktovf1  14312  wwlktovfo  14313  wrd2f1tovbij  14315  dfrtrclrec2  14407  rtrclreclem1  14408  rtrclreclem2  14409  rtrclreclem4  14411  dfrtrcl2  14412  clim  14842  rlim  14843  ello1  14863  elo1  14874  summo  15065  fsum  15068  prodmo  15281  fprod  15286  bpolylem  15393  bpolyval  15394  vdwlem6  16311  vdwlem8  16313  ramcl  16354  strfvnd  16493  prdsplusgval  16737  prdsmulrval  16739  prdsleval  16741  prdsdsval  16742  prdsvscaval  16743  xpsff1o  16831  isacs2  16915  isnat  17208  yonedalem3b  17520  yonedainv  17522  ismhm  17949  prdspjmhm  17984  isgrpinv  18147  pwsmulg  18263  isghm  18349  cayleylem2  18532  symgfix2  18535  gsmsymgrfix  18547  gsmsymgreq  18551  symgfixelq  18552  pmtr3ncomlem2  18593  pmtrdifel  18599  pmtrdifwrdel  18604  pmtrdifwrdel2  18605  psgnunilem2  18614  psgnunilem3  18615  efgsdm  18847  efgredlemd  18861  efgredlem  18864  efgred  18865  efgrelexlema  18866  efgrelexlemb  18867  prdsgsum  19092  isabv  19581  islmhm  19790  frgpcyg  20263  psgndiflemB  20287  psgndiflemA  20288  dsmmelbas  20426  frlmipval  20466  frlmphl  20468  uvcf1  20479  islindf  20499  islindf4  20525  psrmulfval  20621  evlslem2  20749  evlslem3  20750  evlslem1  20752  mpfrcl  20755  selvval  20788  coe1fval  20832  coe1mul2lem2  20895  coe1tm  20900  madetsumid  21064  mvmulval  21146  marepvval0  21169  mulmarep1gsum2  21177  mdetleib2  21191  m1detdiag  21200  mdetralt  21211  mdetunilem7  21221  mdetunilem9  21223  m2detleiblem3  21232  m2detleiblem4  21233  m2detleib  21234  symgmatr01lem  21256  gsummatr01lem1  21258  gsummatr01lem4  21261  gsummatr01  21262  smadiadetlem3  21271  pmatcoe1fsupp  21304  pmatcollpw3lem  21386  pmatcollpw3fi1lem2  21390  iscnp  21840  1stcfb  22048  ptpjpre1  22174  elpt  22175  elptr  22176  ptpjopn  22215  dfac14  22221  upxp  22226  pthaus  22241  ptrescn  22242  xkoptsub  22257  cnmptkp  22283  xkofvcn  22287  cnmptk1p  22288  cnmptk2  22289  ptunhmeo  22411  ptcmplem3  22657  ptcmplem4  22658  symgtgp  22709  prdstmdd  22727  isucn  22882  imasdsf1olem  22978  prdsxmslem2  23134  tngngp3  23260  nmoval  23319  elcncf  23492  ishtpy  23575  pcoval  23614  om1elbas  23635  elpi1i  23649  iscau  23878  rrxds  23995  rrxdsfival  24015  ehl1eudisval  24023  ehl2eudisval  24025  mbfi1fseqlem6  24322  mbfi1flimlem  24324  isibl  24367  deg1ldg  24691  deg1leb  24694  elply2  24791  elplyr  24796  ne0p  24802  coeeu  24820  coelem  24821  coeeq  24822  coeidlem  24832  elqaalem3  24915  qaa  24917  iaa  24919  aareccl  24920  aannenlem2  24923  aaliou2  24934  dchrptlem2  25847  dchrpt  25849  dchrsum2  25850  sumdchr2  25852  dchrvmaeq0  26086  rpvmasum2  26094  dchrisum0re  26095  ostth  26221  iscgrg  26304  isismt  26326  israg  26489  iseqlg  26659  brbtwn  26691  brbtwn2  26697  colinearalg  26702  axsegconlem1  26709  axsegcon  26719  ax5seglem5  26725  axpasch  26733  axlowdim  26753  axeuclidlem  26754  axcontlem1  26756  axcontlem2  26757  axcontlem5  26760  vtxdgfval  27255  1egrvtxdg1  27297  isewlk  27390  iswlk  27398  uspgr2wlkeq2  27434  iswlkon  27445  isclwlk  27560  iscrct  27577  iscycl  27578  iswwlks  27620  wwlknon  27641  wlkiswwlks2  27659  wwlksnredwwlkn0  27680  wlksnwwlknvbij  27692  wwlksnextproplem3  27695  wwlksnextprop  27696  umgr2wlk  27733  midwwlks2s3  27736  elwwlks2  27750  elwspths2spth  27751  rusgrnumwwlkslem  27753  rusgrnumwwlkb0  27755  rusgrnumwwlks  27758  isclwwlk  27767  clwlkclwwlklem1  27782  clwwlkn1loopb  27826  clwwlkel  27829  clwwlkf  27830  clwwlkf1  27832  isclwwlknon  27874  clwwlknon1  27880  s2elclwwlknon2  27887  clwwlkvbij  27896  uhgr3cyclex  27965  fusgreg2wsplem  28116  fusgr2wsp2nb  28117  fusgreghash2wsp  28121  2clwwlkel  28132  extwwlkfabel  28136  numclwwlk1lem2fv  28139  numclwwlk1lem2  28143  clwwlknonclwlknonf1o  28145  dlwwlknondlwlknonf1o  28148  numclwwlk2lem1  28159  numclwlk2lem2f  28160  numclwlk2lem2f1o  28162  ex-fv  28226  isnvlem  28391  islno  28534  nmooval  28544  nmblolbi  28581  isphg  28598  ajmoi  28639  ajval  28642  ubthlem3  28653  htthlem  28698  hcau  28965  hlimi  28969  hosmval  29516  hommval  29517  hodmval  29518  hfsmval  29519  hfmmval  29520  adjmo  29613  nmopval  29637  elcnop  29638  ellnop  29639  elunop  29653  elhmop  29654  nmfnval  29657  elcnfn  29663  ellnfn  29664  adjeu  29670  adjval  29671  eigvecval  29677  eigvalfval  29678  adj1  29714  adjeq  29716  hmopadj2  29722  lnopeq0i  29788  lnopeq  29790  elunop2  29794  lnophm  29800  hmopco  29804  nmbdoplb  29806  nmcoplb  29811  lnopcon  29816  lnfn0  29828  lnfnmul  29829  nmbdfnlb  29831  nmcfnlb  29835  lnfncon  29837  riesz4  29845  riesz1  29846  cnlnadjlem9  29856  cnlnadjeu  29859  cnlnssadj  29861  nmopcoi  29876  bra11  29889  cnvbraval  29891  pjss2coi  29945  pjssdif2i  29955  pjssdif1i  29956  pjclem4  29980  pj3si  29988  pj3cor1i  29990  isst  29994  ishst  29995  stri  30038  hstri  30046  aciunf1lem  30415  ismnt  30675  mgcval  30679  linds2eq  30976  lbsdiflsp0  31079  fedgmullem1  31082  fedgmullem2  31083  fedgmul  31084  lmatval  31135  mdetpmtr1  31145  ismeas  31532  isrnmeas  31533  cntnevol  31561  carsgval  31635  sitgval  31664  eulerpartleme  31695  eulerpartlemd  31698  eulerpartlemr  31706  eulerpartlemgvv  31708  eulerpart  31714  cndprobval  31765  signstfvneq0  31916  reprsum  31958  reprsuc  31960  reprpmtf1o  31971  reprdifc  31972  breprexp  31978  vtsval  31982  hgt750lemb  32001  hgt750lema  32002  hgt750leme  32003  bnj66  32206  bnj106  32214  bnj125  32218  bnj154  32224  bnj155  32225  bnj526  32234  bnj540  32238  bnj609  32263  bnj611  32264  bnj893  32274  bnj1000  32287  bnj1014  32307  bnj1015  32308  bnj1234  32359  bnj1463  32401  loop1cycl  32458  derangenlem  32492  subfacp1lem3  32503  subfacp1lem5  32505  subfacp1lem6  32506  subfacp1  32507  sconnpht  32550  cnpconn  32551  txpconn  32553  ptpconn  32554  indispconn  32555  connpconn  32556  cvxpconn  32563  cvmliftmo  32605  cvmliftlem14  32618  cvmliftlem15  32619  cvmliftiota  32622  cvmlift2  32637  cvmliftphtlem  32638  cvmlift3lem2  32641  cvmlift3lem6  32645  cvmlift3lem7  32646  cvmlift3lem9  32648  cvmlift3  32649  satfv1lem  32683  satfv1  32684  sategoelfvb  32740  mrsubff1  32835  mrsub0  32837  mrsubccat  32839  mrsubcn  32840  elmsubrn  32849  msubrn  32850  msubco  32852  msubvrs  32881  mclsax  32890  shftvalg  33037  poseq  33169  soseq  33170  frrlem1  33197  frrlem13  33209  sltval  33228  nolesgn2o  33252  noresle  33274  noprefixmo  33276  nosupfv  33280  fwddifval  33697  fwddifnval  33698  bj-evalval  34451  unceq  34992  matunitlindflem2  35012  poimirlem17  35032  poimirlem20  35035  poimirlem22  35037  poimirlem23  35038  poimirlem27  35042  poimirlem28  35043  poimirlem30  35045  poimirlem31  35046  poimirlem32  35047  poimir  35048  broucube  35049  voliunnfl  35059  volsupnfl  35060  itg2addnclem  35066  itg2addnclem3  35068  itg2addnc  35069  ftc1anclem2  35089  ftc1anclem5  35092  eqfnun  35118  upixp  35125  fdc  35141  isismty  35197  rrnmval  35224  elghomlem2OLD  35282  isrngohom  35361  islfl  36314  isopos  36434  islaut  37337  ispautN  37353  isldil  37364  isltrn  37373  ltrnid  37389  ltrneq2  37402  isdilN  37408  istrnN  37411  trlval  37416  ltrneq3  37462  cdleme50ex  37813  cdleme  37814  cdlemg1a  37824  ltrniotaval  37835  ltrniotavalbN  37838  cdlemeiota  37839  cdlemg2jlemOLDN  37847  cdlemg2fvlem  37848  cdlemg2klem  37849  istendo  38014  tendoplcbv  38029  tendopl  38030  tendoicbv  38047  tendoi  38048  tendoid0  38079  tendo1ne0  38082  cdlemksv2  38101  cdlemkuv2  38121  cdlemk33N  38163  cdlemk34  38164  cdlemk36  38167  cdlemk19u  38224  cdlemk  38228  tendoex  38229  dvavsca  38271  dvhvscacbv  38352  dvhvscaval  38353  dicopelval  38431  dicelval1sta  38441  diclspsn  38448  dihmeetlem13N  38573  dih1dimatlem0  38582  dih1dimatlem  38583  dihpN  38590  islpolN  38737  hdmap1fval  39050  hdmapfval  39081  frlmsnic  39400  uvcn0  39402  ismrc  39572  mzpclval  39596  mzpsubst  39619  mzprename  39620  mzpcompact2lem  39622  eldioph  39629  eldioph2  39633  eldioph2b  39634  eldioph3  39637  rexrabdioph  39665  2rexfrabdioph  39667  3rexfrabdioph  39668  4rexfrabdioph  39669  6rexfrabdioph  39670  7rexfrabdioph  39671  eldioph4i  39683  rabren3dioph  39686  mzpcong  39843  jm2.27dlem1  39880  wepwsolem  39916  aomclem6  39933  aomclem8  39935  dfac11  39936  dgraalem  40019  dgraaub  40022  dgraa0p  40023  mpaaeu  40024  mpaalem  40026  aaitgo  40036  rngunsnply  40047  eliunov2  40310  rfovcnvfvd  40639  fsovfvd  40642  fsovcnvlem  40645  dssmapfv2d  40650  dssmapnvod  40652  clsk1independent  40682  ntrclskb  40705  ntrclsk13  40707  gneispace2  40768  mnringmulrvald  40869  dvconstbi  40972  addrval  41104  subrval  41105  mulvval  41106  fnchoice  41592  refsum2cnlem1  41600  choicefi  41767  axccdom  41791  fmulcl  42162  fmuldfeqlem1  42163  mccllem  42178  mccl  42179  climf  42203  climf2  42247  dvnprodlem1  42527  dvnprodlem3  42529  dvnprod  42530  stoweidlem2  42583  stoweidlem6  42587  stoweidlem8  42589  stoweidlem9  42590  stoweidlem15  42596  stoweidlem16  42597  stoweidlem17  42598  stoweidlem18  42599  stoweidlem21  42602  stoweidlem27  42608  stoweidlem31  42612  stoweidlem36  42617  stoweidlem37  42618  stoweidlem41  42622  stoweidlem43  42624  stoweidlem44  42625  stoweidlem45  42626  stoweidlem46  42627  stoweidlem48  42629  stoweidlem51  42632  stoweidlem55  42636  stoweidlem59  42640  stoweidlem60  42641  stoweidlem62  42643  fourierdlem2  42690  fourierdlem3  42691  elaa2lem  42814  etransclem11  42826  etransclem24  42839  etransclem26  42841  etransclem28  42843  etransclem35  42850  rrndistlt  42871  ioorrnopn  42886  subsaliuncllem  42936  sge0val  42944  ismea  43029  caragenval  43071  isome  43072  isomenndlem  43108  hoicvrrex  43134  ovnlecvr  43136  ovncvrrp  43142  ovn0lem  43143  ovnsubaddlem1  43148  ovnsubadd  43150  hsphoif  43154  hoidmvval  43155  hsphoival  43157  hoidmvlelem3  43175  hoidmvlelem5  43177  hoidmvle  43178  ovnhoilem1  43179  ovnhoi  43181  ovnlecvr2  43188  ovncvr2  43189  hoidifhspval2  43193  hoiqssbllem2  43201  hspmbllem2  43205  hspmbllem3  43206  hspmbl  43207  ovnovollem1  43234  smfmullem2  43363  smfmul  43366  smfpimcclem  43377  iccpart  43872  iccpartiun  43890  icceuelpart  43892  nnsum3primes4  44245  nnsum3primesgbe  44249  nnsum4primesodd  44253  nnsum4primesoddALTV  44254  nnsum4primeseven  44257  nnsum4primesevenALTV  44258  bgoldbtbnd  44266  isomgreqve  44282  isomushgr  44283  isomuspgrlem2  44290  isomgrsym  44293  isomgrtr  44296  ushrisomgr  44298  isupwlk  44303  ismgmhm  44342  isrnghm  44455  lincval  44757  lincdifsn  44772  linindslinci  44796  lindslinindsimp1  44805  linds0  44813  el0ldep  44814  lindsrng01  44816  snlindsntorlem  44818  ldepspr  44821  islindeps2  44831  zlmodzxzldep  44852  bigoval  44902  elbigo  44904  0aryfvalelfv  44988  1arympt1fv  44992  1arymaptfv  44993  1arymaptfo  44996  2arymptfv  45003  2arymaptfv  45004  2arymaptfo  45007  prelrrx2b  45067  rrx2plord  45073  rrx2vlinest  45094  rrx2linesl  45096  elrrx2linest2  45098  line2ylem  45104  line2xlem  45106  itsclc0  45124  itsclc0b  45125  itscnhlinecirc02p  45138  setrecseq  45154  aacllem  45268
  Copyright terms: Public domain W3C validator