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

Theorem fveq1 6663
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 5060 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 6333 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 6357 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 6357 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2881 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528   class class class wbr 5058  cio 6306  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-rex 3144  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357
This theorem is referenced by:  fveq1i  6665  fveq1d  6666  iffv  6681  fvmptd3f  6776  fvmptdv2  6779  fsnex  7030  f1prex  7031  isoeq1  7059  oveq  7151  elovmpt3imp  7391  offval  7405  ofrfval  7406  offval3  7674  bropopvvv  7776  bropfvvvvlem  7777  wfrlem1  7945  wfrlem3a  7948  wfrlem15  7960  smoeq  7978  tfrlem12  8016  tz7.44-2  8034  tz7.44-3  8035  rdgeq1  8038  mapsncnv  8446  elixp2  8454  resixpfo  8489  elixpsn  8490  mapsnend  8577  enfixsn  8615  mapxpen  8672  ac6sfi  8751  ordtypelem7  8977  wemaplem1  8999  ixpiunwdom  9044  oemapval  9135  cantnf  9145  wemapwe  9149  cnfcom3clem  9157  updjud  9352  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  13016  axdc4uzlem  13341  seqeq3  13364  seqof  13417  ccatfval  13915  wrdl1s1  13958  ccat1st1st  13974  cshf1  14162  cshweqrep  14173  wrdlen2i  14294  wwlktovf  14310  wwlktovf1  14311  wwlktovfo  14312  wrd2f1tovbij  14314  dfrtrclrec2  14406  rtrclreclem1  14407  rtrclreclem2  14408  rtrclreclem4  14410  dfrtrcl2  14411  clim  14841  rlim  14842  ello1  14862  elo1  14873  summo  15064  fsum  15067  prodmo  15280  fprod  15285  bpolylem  15392  bpolyval  15393  vdwlem6  16312  vdwlem8  16314  ramcl  16355  strfvnd  16492  prdsplusgval  16736  prdsmulrval  16738  prdsleval  16740  prdsdsval  16741  prdsvscaval  16742  xpsff1o  16830  isacs2  16914  isnat  17207  yonedalem3b  17519  yonedainv  17521  ismhm  17948  prdspjmhm  17983  isgrpinv  18096  pwsmulg  18212  isghm  18298  cayleylem2  18472  symgfix2  18475  gsmsymgrfix  18487  gsmsymgreq  18491  symgfixelq  18492  pmtr3ncomlem2  18533  pmtrdifel  18539  pmtrdifwrdel  18544  pmtrdifwrdel2  18545  psgnunilem2  18554  psgnunilem3  18555  efgsdm  18787  efgredlemd  18801  efgredlem  18804  efgred  18805  efgrelexlema  18806  efgrelexlemb  18807  prdsgsum  19032  isabv  19521  islmhm  19730  psrmulfval  20095  evlslem2  20222  evlslem3  20223  evlslem1  20225  mpfrcl  20228  selvval  20261  coe1fval  20303  coe1mul2lem2  20366  coe1tm  20371  frgpcyg  20650  psgndiflemB  20674  psgndiflemA  20675  dsmmelbas  20813  frlmipval  20853  frlmphl  20855  uvcf1  20866  islindf  20886  islindf4  20912  madetsumid  21000  mvmulval  21082  marepvval0  21105  mulmarep1gsum2  21113  mdetleib2  21127  m1detdiag  21136  mdetralt  21147  mdetunilem7  21157  mdetunilem9  21159  m2detleiblem3  21168  m2detleiblem4  21169  m2detleib  21170  symgmatr01lem  21192  gsummatr01lem1  21194  gsummatr01lem4  21197  gsummatr01  21198  smadiadetlem3  21207  pmatcoe1fsupp  21239  pmatcollpw3lem  21321  pmatcollpw3fi1lem2  21325  iscnp  21775  1stcfb  21983  ptpjpre1  22109  elpt  22110  elptr  22111  ptpjopn  22150  dfac14  22156  upxp  22161  pthaus  22176  ptrescn  22177  xkoptsub  22192  cnmptkp  22218  xkofvcn  22222  cnmptk1p  22223  cnmptk2  22224  ptunhmeo  22346  ptcmplem3  22592  ptcmplem4  22593  symgtgp  22639  prdstmdd  22661  isucn  22816  imasdsf1olem  22912  prdsxmslem2  23068  tngngp3  23194  nmoval  23253  elcncf  23426  ishtpy  23505  pcoval  23544  om1elbas  23565  elpi1i  23579  iscau  23808  rrxds  23925  rrxdsfival  23945  ehl1eudisval  23953  ehl2eudisval  23955  mbfi1fseqlem6  24250  mbfi1flimlem  24252  isibl  24295  deg1ldg  24615  deg1leb  24618  elply2  24715  elplyr  24720  ne0p  24726  coeeu  24744  coelem  24745  coeeq  24746  coeidlem  24756  elqaalem3  24839  qaa  24841  iaa  24843  aareccl  24844  aannenlem2  24847  aaliou2  24858  dchrptlem2  25769  dchrpt  25771  dchrsum2  25772  sumdchr2  25774  dchrvmaeq0  26008  rpvmasum2  26016  dchrisum0re  26017  ostth  26143  iscgrg  26226  isismt  26248  israg  26411  iseqlg  26581  brbtwn  26613  brbtwn2  26619  colinearalg  26624  axsegconlem1  26631  axsegcon  26641  ax5seglem5  26647  axpasch  26655  axlowdim  26675  axeuclidlem  26676  axcontlem1  26678  axcontlem2  26679  axcontlem5  26682  vtxdgfval  27177  1egrvtxdg1  27219  isewlk  27312  iswlk  27320  uspgr2wlkeq2  27356  iswlkon  27367  isclwlk  27482  iscrct  27499  iscycl  27500  iswwlks  27542  wwlknon  27563  wlkiswwlks2  27581  wwlksnredwwlkn0  27602  wlksnwwlknvbij  27615  wwlksnextproplem3  27618  wwlksnextprop  27619  umgr2wlk  27656  midwwlks2s3  27659  elwwlks2  27673  elwspths2spth  27674  rusgrnumwwlkslem  27676  rusgrnumwwlkb0  27678  rusgrnumwwlks  27681  isclwwlk  27690  clwlkclwwlklem1  27705  clwwlkn1loopb  27749  clwwlkel  27753  clwwlkf  27754  clwwlkf1  27756  isclwwlknon  27798  clwwlknon1  27804  s2elclwwlknon2  27811  clwwlkvbij  27820  uhgr3cyclex  27889  fusgreg2wsplem  28040  fusgr2wsp2nb  28041  fusgreghash2wsp  28045  2clwwlkel  28056  extwwlkfabel  28060  numclwwlk1lem2fv  28063  numclwwlk1lem2  28067  clwwlknonclwlknonf1o  28069  dlwwlknondlwlknonf1o  28072  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  ex-fv  28150  isnvlem  28315  islno  28458  nmooval  28468  nmblolbi  28505  isphg  28522  ajmoi  28563  ajval  28566  ubthlem3  28577  htthlem  28622  hcau  28889  hlimi  28893  hosmval  29440  hommval  29441  hodmval  29442  hfsmval  29443  hfmmval  29444  adjmo  29537  nmopval  29561  elcnop  29562  ellnop  29563  elunop  29577  elhmop  29578  nmfnval  29581  elcnfn  29587  ellnfn  29588  adjeu  29594  adjval  29595  eigvecval  29601  eigvalfval  29602  adj1  29638  adjeq  29640  hmopadj2  29646  lnopeq0i  29712  lnopeq  29714  elunop2  29718  lnophm  29724  hmopco  29728  nmbdoplb  29730  nmcoplb  29735  lnopcon  29740  lnfn0  29752  lnfnmul  29753  nmbdfnlb  29755  nmcfnlb  29759  lnfncon  29761  riesz4  29769  riesz1  29770  cnlnadjlem9  29780  cnlnadjeu  29783  cnlnssadj  29785  nmopcoi  29800  bra11  29813  cnvbraval  29815  pjss2coi  29869  pjssdif2i  29879  pjssdif1i  29880  pjclem4  29904  pj3si  29912  pj3cor1i  29914  isst  29918  ishst  29919  stri  29962  hstri  29970  aciunf1lem  30336  linds2eq  30869  lbsdiflsp0  30922  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  lmatval  30978  mdetpmtr1  30988  ismeas  31358  isrnmeas  31359  cntnevol  31387  carsgval  31461  sitgval  31490  eulerpartleme  31521  eulerpartlemd  31524  eulerpartlemr  31532  eulerpartlemgvv  31534  eulerpart  31540  cndprobval  31591  signstfvneq0  31742  reprsum  31784  reprsuc  31786  reprpmtf1o  31797  reprdifc  31798  breprexp  31804  vtsval  31808  hgt750lemb  31827  hgt750lema  31828  hgt750leme  31829  bnj66  32032  bnj106  32040  bnj125  32044  bnj154  32050  bnj155  32051  bnj526  32060  bnj540  32064  bnj609  32089  bnj611  32090  bnj893  32100  bnj1000  32113  bnj1014  32132  bnj1015  32133  bnj1234  32183  bnj1463  32225  loop1cycl  32282  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  subfacp1lem6  32330  subfacp1  32331  sconnpht  32374  cnpconn  32375  txpconn  32377  ptpconn  32378  indispconn  32379  connpconn  32380  cvxpconn  32387  cvmliftmo  32429  cvmliftlem14  32442  cvmliftlem15  32443  cvmliftiota  32446  cvmlift2  32461  cvmliftphtlem  32462  cvmlift3lem2  32465  cvmlift3lem6  32469  cvmlift3lem7  32470  cvmlift3lem9  32472  cvmlift3  32473  satfv1lem  32507  satfv1  32508  sategoelfvb  32564  mrsubff1  32659  mrsub0  32661  mrsubccat  32663  mrsubcn  32664  elmsubrn  32673  msubrn  32674  msubco  32676  msubvrs  32705  mclsax  32714  shftvalg  32861  poseq  32993  soseq  32994  frrlem1  33021  frrlem13  33033  sltval  33052  nolesgn2o  33076  noresle  33098  noprefixmo  33100  nosupfv  33104  fwddifval  33521  fwddifnval  33522  bj-evalval  34261  unceq  34751  matunitlindflem2  34771  poimirlem17  34791  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimirlem27  34801  poimirlem28  34802  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  poimir  34807  broucube  34808  voliunnfl  34818  volsupnfl  34819  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  ftc1anclem2  34850  ftc1anclem5  34853  eqfnun  34880  upixp  34887  fdc  34903  isismty  34962  rrnmval  34989  elghomlem2OLD  35047  isrngohom  35126  islfl  36078  isopos  36198  islaut  37101  ispautN  37117  isldil  37128  isltrn  37137  ltrnid  37153  ltrneq2  37166  isdilN  37172  istrnN  37175  trlval  37180  ltrneq3  37226  cdleme50ex  37577  cdleme  37578  cdlemg1a  37588  ltrniotaval  37599  ltrniotavalbN  37602  cdlemeiota  37603  cdlemg2jlemOLDN  37611  cdlemg2fvlem  37612  cdlemg2klem  37613  istendo  37778  tendoplcbv  37793  tendopl  37794  tendoicbv  37811  tendoi  37812  tendoid0  37843  tendo1ne0  37846  cdlemksv2  37865  cdlemkuv2  37885  cdlemk33N  37927  cdlemk34  37928  cdlemk36  37931  cdlemk19u  37988  cdlemk  37992  tendoex  37993  dvavsca  38035  dvhvscacbv  38116  dvhvscaval  38117  dicopelval  38195  dicelval1sta  38205  diclspsn  38212  dihmeetlem13N  38337  dih1dimatlem0  38346  dih1dimatlem  38347  dihpN  38354  islpolN  38501  hdmap1fval  38814  hdmapfval  38845  frlmsnic  39029  uvcn0  39031  ismrc  39178  mzpclval  39202  mzpsubst  39225  mzprename  39226  mzpcompact2lem  39228  eldioph  39235  eldioph2  39239  eldioph2b  39240  eldioph3  39243  rexrabdioph  39271  2rexfrabdioph  39273  3rexfrabdioph  39274  4rexfrabdioph  39275  6rexfrabdioph  39276  7rexfrabdioph  39277  eldioph4i  39289  rabren3dioph  39292  mzpcong  39449  jm2.27dlem1  39486  wepwsolem  39522  aomclem6  39539  aomclem8  39541  dfac11  39542  dgraalem  39625  dgraaub  39628  dgraa0p  39629  mpaaeu  39630  mpaalem  39632  aaitgo  39642  rngunsnply  39653  eliunov2  39904  rfovcnvfvd  40233  fsovfvd  40236  fsovcnvlem  40239  dssmapfv2d  40244  dssmapnvod  40246  clsk1independent  40276  ntrclskb  40299  ntrclsk13  40301  gneispace2  40362  dvconstbi  40546  addrval  40678  subrval  40679  mulvval  40680  fnchoice  41166  refsum2cnlem1  41174  choicefi  41343  axccdom  41367  fmulcl  41742  fmuldfeqlem1  41743  mccllem  41758  mccl  41759  climf  41783  climf2  41827  dvnprodlem1  42111  dvnprodlem3  42113  dvnprod  42114  stoweidlem2  42168  stoweidlem6  42172  stoweidlem8  42174  stoweidlem9  42175  stoweidlem15  42181  stoweidlem16  42182  stoweidlem17  42183  stoweidlem18  42184  stoweidlem21  42187  stoweidlem27  42193  stoweidlem31  42197  stoweidlem36  42202  stoweidlem37  42203  stoweidlem41  42207  stoweidlem43  42209  stoweidlem44  42210  stoweidlem45  42211  stoweidlem46  42212  stoweidlem48  42214  stoweidlem51  42217  stoweidlem55  42221  stoweidlem59  42225  stoweidlem60  42226  stoweidlem62  42228  fourierdlem2  42275  fourierdlem3  42276  elaa2lem  42399  etransclem11  42411  etransclem24  42424  etransclem26  42426  etransclem28  42428  etransclem35  42435  rrndistlt  42456  ioorrnopn  42471  subsaliuncllem  42521  sge0val  42529  ismea  42614  caragenval  42656  isome  42657  isomenndlem  42693  hoicvrrex  42719  ovnlecvr  42721  ovncvrrp  42727  ovn0lem  42728  ovnsubaddlem1  42733  ovnsubadd  42735  hsphoif  42739  hoidmvval  42740  hsphoival  42742  hoidmvlelem3  42760  hoidmvlelem5  42762  hoidmvle  42763  ovnhoilem1  42764  ovnhoi  42766  ovnlecvr2  42773  ovncvr2  42774  hoidifhspval2  42778  hoiqssbllem2  42786  hspmbllem2  42790  hspmbllem3  42791  hspmbl  42792  ovnovollem1  42819  smfmullem2  42948  smfmul  42951  smfpimcclem  42962  iccpart  43423  iccpartiun  43441  icceuelpart  43443  nnsum3primes4  43800  nnsum3primesgbe  43804  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbnd  43821  isomgreqve  43837  isomushgr  43838  isomuspgrlem2  43845  isomgrsym  43848  isomgrtr  43851  ushrisomgr  43853  isupwlk  43858  ismgmhm  43897  isrnghm  44061  lincval  44362  lincdifsn  44377  linindslinci  44401  lindslinindsimp1  44410  linds0  44418  el0ldep  44419  lindsrng01  44421  snlindsntorlem  44423  ldepspr  44426  islindeps2  44436  zlmodzxzldep  44457  bigoval  44507  elbigo  44509  prelrrx2b  44599  rrx2plord  44605  rrx2vlinest  44626  rrx2linesl  44628  elrrx2linest2  44630  line2ylem  44636  line2xlem  44638  itsclc0  44656  itsclc0b  44657  itscnhlinecirc02p  44670  setrecseq  44686  aacllem  44800
  Copyright terms: Public domain W3C validator