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

Theorem fveq1 6157
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 4625 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 5841 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 5865 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5865 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2680 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480   class class class wbr 4623  cio 5818  cfv 5857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2914  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865
This theorem is referenced by:  fveq1i  6159  fveq1d  6160  iffv  6172  fvmptdf  6262  fvmptdv2  6264  fsnex  6503  f1prex  6504  isoeq1  6532  oveq  6621  elovmpt3imp  6855  offval  6869  ofrfval  6870  offval3  7122  bropopvvv  7215  bropfvvvvlem  7216  wfrlem1  7374  wfrlem3a  7377  wfrlem15  7389  smoeq  7407  tfrlem12  7445  tz7.44-2  7463  tz7.44-3  7464  rdgeq1  7467  mapsncnv  7864  elixp2  7872  resixpfo  7906  elixpsn  7907  mapsnen  7995  enfixsn  8029  mapxpen  8086  ac6sfi  8164  ordtypelem7  8389  wemaplem1  8411  ixpiunwdom  8456  oemapval  8540  cantnf  8550  wemapwe  8554  cnfcom3clem  8562  infxpenc2lem2  8803  fseqenlem1  8807  dfac8clem  8815  ac5num  8819  acni  8828  acni2  8829  acnlem  8831  dfac4  8905  dfac5lem5  8910  dfac2a  8912  dfac9  8918  dfacacn  8923  dfac12lem1  8925  dfac12r  8928  cofsmo  9051  cfsmolem  9052  cfsmo  9053  cfcoflem  9054  coftr  9055  alephsing  9058  isfin3ds  9111  fin23lem17  9120  fin23lem32  9126  fin23lem39  9132  isf33lem  9148  isf34lem6  9162  axcc2lem  9218  axcc3  9220  axdc2lem  9230  axdc3lem2  9233  axdc3lem3  9234  axdc3  9236  axdc4lem  9237  axcclem  9239  ac6num  9261  axdclem2  9302  konigthlem  9350  inar1  9557  1fv  12415  axdc4uzlem  12738  seqeq3  12762  seqof  12814  ccatfval  13313  wrdl1s1  13349  cshf1  13509  cshweqrep  13520  wrdlen2i  13636  wwlktovf  13649  wwlktovf1  13650  wwlktovfo  13651  wrd2f1tovbij  13653  dfrtrclrec2  13747  rtrclreclem1  13748  rtrclreclem2  13749  rtrclreclem4  13751  dfrtrcl2  13752  clim  14175  rlim  14176  ello1  14196  elo1  14207  summo  14397  fsum  14400  prodmo  14610  fprod  14615  bpolylem  14723  bpolyval  14724  vdwlem6  15633  vdwlem8  15635  ramcl  15676  strfvnd  15818  prdsplusgval  16073  prdsmulrval  16075  prdsleval  16077  prdsdsval  16078  prdsvscaval  16079  xpsff1o  16168  isacs2  16254  isnat  16547  yonedalem3b  16859  yonedainv  16861  ismhm  17277  prdspjmhm  17307  isgrpinv  17412  pwsmulg  17527  isghm  17600  cayleylem2  17773  symgfix2  17776  gsmsymgrfix  17788  gsmsymgreq  17792  symgfixelq  17793  pmtr3ncomlem2  17834  pmtrdifel  17840  pmtrdifwrdel  17845  pmtrdifwrdel2  17846  psgnunilem2  17855  psgnunilem3  17856  efgsdm  18083  efgredlemd  18097  efgredlem  18100  efgred  18101  efgrelexlema  18102  efgrelexlemb  18103  prdsgsum  18317  isabv  18759  islmhm  18967  psrmulfval  19325  evlslem2  19452  evlslem3  19454  evlslem1  19455  mpfrcl  19458  coe1fval  19515  coe1mul2lem2  19578  coe1tm  19583  frgpcyg  19862  psgndiflemB  19886  psgndiflemA  19887  dsmmelbas  20023  frlmipval  20058  frlmphl  20060  uvcf1  20071  islindf  20091  islindf4  20117  madetsumid  20207  mvmulval  20289  marepvval0  20312  mulmarep1gsum2  20320  mdetleib2  20334  m1detdiag  20343  mdetralt  20354  mdetunilem7  20364  mdetunilem9  20366  m2detleiblem3  20375  m2detleiblem4  20376  m2detleib  20377  symgmatr01lem  20399  gsummatr01lem1  20401  gsummatr01lem4  20404  gsummatr01  20405  smadiadetlem3  20414  pmatcoe1fsupp  20446  pmatcollpw3lem  20528  pmatcollpw3fi1lem2  20532  iscnp  20981  1stcfb  21188  ptpjpre1  21314  elpt  21315  elptr  21316  ptpjopn  21355  dfac14  21361  upxp  21366  pthaus  21381  ptrescn  21382  xkoptsub  21397  cnmptkp  21423  xkofvcn  21427  cnmptk1p  21428  cnmptk2  21429  ptunhmeo  21551  ptcmplem3  21798  ptcmplem4  21799  symgtgp  21845  prdstmdd  21867  isucn  22022  imasdsf1olem  22118  prdsxmslem2  22274  tngngp3  22400  nmoval  22459  elcncf  22632  ishtpy  22711  pcoval  22751  om1elbas  22772  elpi1i  22786  iscau  23014  rrxds  23121  mbfi1fseqlem6  23427  mbfi1flimlem  23429  isibl  23472  deg1ldg  23790  deg1leb  23793  elply2  23890  elplyr  23895  ne0p  23901  coeeu  23919  coelem  23920  coeeq  23921  coeidlem  23931  elqaalem3  24014  qaa  24016  iaa  24018  aareccl  24019  aannenlem2  24022  aaliou2  24033  dchrptlem2  24924  dchrpt  24926  dchrsum2  24927  sumdchr2  24929  dchrvmaeq0  25127  rpvmasum2  25135  dchrisum0re  25136  ostth  25262  iscgrg  25341  isismt  25363  israg  25526  iseqlg  25681  brbtwn  25713  brbtwn2  25719  colinearalg  25724  axsegconlem1  25731  axsegcon  25741  ax5seglem5  25747  axpasch  25755  axlowdim  25775  axeuclidlem  25776  axcontlem1  25778  axcontlem2  25779  axcontlem5  25782  vtxdgfval  26284  1egrvtxdg1  26325  isewlk  26402  iswlk  26410  uspgr2wlkeq2  26446  iswlkon  26456  isclwlk  26572  iscrct  26588  iscycl  26589  iswwlks  26631  wwlknon  26645  wlkiswwlks2  26664  wlkwwlkfun  26684  wlkwwlksur  26686  wlkwwlkbij2  26688  wwlksnredwwlkn0  26694  wlksnwwlknvbij  26706  wwlksnextproplem3  26709  wwlksnextprop  26710  umgr2wlk  26748  wwlks2onv  26750  elwwlks2  26762  elwspths2spth  26763  rusgrnumwwlkslem  26765  rusgrnumwwlkb0  26767  rusgrnumwwlks  26770  isclwwlks  26781  clwlkclwwlklem1  26801  clwwlksel  26814  clwwlksf  26815  clwwlksf1  26817  clwwlksvbij  26822  clwwlksnun  26874  uhgr3cyclex  26942  fusgr2wsp2nb  27090  fusgreg2wsp  27092  2wspmdisj  27093  fusgreghash2wsp  27094  numclwwlkovfel2  27106  numclwwlkovgel  27111  extwwlkfab  27112  numclwlk1lem2foa  27113  numclwlk1lem2fv  27115  numclwwlk2lem1  27124  numclwlk2lem2f  27125  numclwlk2lem2f1o  27127  numclwwlk5  27134  numclwwlk6  27136  ex-fv  27188  isnvlem  27353  islno  27496  nmooval  27506  nmblolbi  27543  isphg  27560  ajmoi  27602  ajval  27605  ubthlem3  27616  htthlem  27662  hcau  27929  hlimi  27933  hosmval  28482  hommval  28483  hodmval  28484  hfsmval  28485  hfmmval  28486  adjmo  28579  nmopval  28603  elcnop  28604  ellnop  28605  elunop  28619  elhmop  28620  nmfnval  28623  elcnfn  28629  ellnfn  28630  adjeu  28636  adjval  28637  eigvecval  28643  eigvalfval  28644  adj1  28680  adjeq  28682  hmopadj2  28688  lnopeq0i  28754  lnopeq  28756  elunop2  28760  lnophm  28766  hmopco  28770  nmbdoplb  28772  nmcoplb  28777  lnopcon  28782  lnfn0  28794  lnfnmul  28795  nmbdfnlb  28797  nmcfnlb  28801  lnfncon  28803  riesz4  28811  riesz1  28812  cnlnadjlem9  28822  cnlnadjeu  28825  cnlnssadj  28827  nmopcoi  28842  bra11  28855  cnvbraval  28857  pjss2coi  28911  pjssdif2i  28921  pjssdif1i  28922  pjclem4  28946  pj3si  28954  pj3cor1i  28956  isst  28960  ishst  28961  stri  29004  hstri  29012  aciunf1lem  29345  lmatval  29703  mdetpmtr1  29713  ismeas  30085  isrnmeas  30086  cntnevol  30114  carsgval  30188  sitgval  30217  eulerpartleme  30248  eulerpartlemd  30251  eulerpartlemr  30259  eulerpartlemgvv  30261  eulerpart  30267  cndprobval  30318  signstfvneq0  30471  breprsum  30499  breprsuc  30501  bnj66  30691  bnj106  30699  bnj125  30703  bnj154  30709  bnj155  30710  bnj526  30719  bnj540  30723  bnj609  30748  bnj611  30749  bnj893  30759  bnj1000  30772  bnj1014  30791  bnj1015  30792  bnj1234  30842  bnj1463  30884  derangenlem  30914  subfacp1lem3  30925  subfacp1lem5  30927  subfacp1lem6  30928  subfacp1  30929  sconnpht  30972  cnpconn  30973  txpconn  30975  ptpconn  30976  indispconn  30977  connpconn  30978  cvxpconn  30985  cvmliftmo  31027  cvmliftlem14  31040  cvmliftlem15  31041  cvmliftiota  31044  cvmlift2  31059  cvmliftphtlem  31060  cvmlift3lem2  31063  cvmlift3lem6  31067  cvmlift3lem7  31068  cvmlift3lem9  31070  cvmlift3  31071  mrsubff1  31172  mrsub0  31174  mrsubccat  31176  mrsubcn  31177  elmsubrn  31186  msubrn  31187  msubco  31189  msubvrs  31218  mclsax  31227  shftvalg  31378  poseq  31504  soseq  31505  frrlem1  31534  sltval  31554  nobndlem6  31613  noreslege  31624  noprefixmo  31626  nosifv  31629  fwddifval  31964  fwddifnval  31965  unceq  33057  matunitlindflem2  33077  poimirlem17  33097  poimirlem20  33100  poimirlem22  33102  poimirlem23  33103  poimirlem27  33107  poimirlem28  33108  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  poimir  33113  broucube  33114  voliunnfl  33124  volsupnfl  33125  itg2addnclem  33132  itg2addnclem3  33134  itg2addnc  33135  ftc1anclem2  33157  ftc1anclem5  33160  eqfnun  33187  upixp  33195  fdc  33212  isismty  33271  rrnmval  33298  elghomlem2OLD  33356  isrngohom  33435  islfl  33866  isopos  33986  islaut  34888  ispautN  34904  isldil  34915  isltrn  34924  ltrnid  34940  ltrneq2  34953  isdilN  34960  istrnN  34963  trlval  34968  ltrneq3  35014  cdleme50ex  35366  cdleme  35367  cdlemg1a  35377  ltrniotaval  35388  ltrniotavalbN  35391  cdlemeiota  35392  cdlemg2jlemOLDN  35400  cdlemg2fvlem  35401  cdlemg2klem  35402  istendo  35567  tendoplcbv  35582  tendopl  35583  tendoicbv  35600  tendoi  35601  tendoid0  35632  tendo1ne0  35635  cdlemksv2  35654  cdlemkuv2  35674  cdlemk33N  35716  cdlemk34  35717  cdlemk36  35720  cdlemk19u  35777  cdlemk  35781  tendoex  35782  dvavsca  35824  dvhvscacbv  35906  dvhvscaval  35907  dicopelval  35985  dicelval1sta  35995  diclspsn  36002  dihmeetlem13N  36127  dih1dimatlem0  36136  dih1dimatlem  36137  dihpN  36144  islpolN  36291  hdmap1fval  36605  hdmapfval  36638  ismrc  36783  mzpclval  36807  mzpsubst  36830  mzprename  36831  mzpcompact2lem  36833  eldioph  36840  eldioph2  36844  eldioph2b  36845  eldioph3  36848  rexrabdioph  36877  2rexfrabdioph  36879  3rexfrabdioph  36880  4rexfrabdioph  36881  6rexfrabdioph  36882  7rexfrabdioph  36883  eldioph4i  36895  rabren3dioph  36898  mzpcong  37058  jm2.27dlem1  37095  wepwsolem  37131  aomclem6  37148  aomclem8  37150  dfac11  37151  dgraalem  37235  dgraaub  37238  dgraa0p  37239  mpaaeu  37240  mpaalem  37242  aaitgo  37252  rngunsnply  37263  eliunov2  37491  rfovcnvfvd  37822  fsovfvd  37825  fsovcnvlem  37828  dssmapfv2d  37833  dssmapnvod  37835  clsk1independent  37865  ntrclskb  37888  ntrclsk13  37890  gneispace2  37951  dvconstbi  38054  addrval  38191  subrval  38192  mulvval  38193  fnchoice  38710  refsum2cnlem1  38718  mapsnend  38900  choicefi  38901  axccdom  38925  fmulcl  39249  fmuldfeqlem1  39250  mccllem  39265  mccl  39266  climf  39290  climf2  39334  dvnprodlem1  39498  dvnprodlem3  39500  dvnprod  39501  stoweidlem2  39556  stoweidlem6  39560  stoweidlem8  39562  stoweidlem9  39563  stoweidlem15  39569  stoweidlem16  39570  stoweidlem17  39571  stoweidlem18  39572  stoweidlem21  39575  stoweidlem27  39581  stoweidlem31  39585  stoweidlem36  39590  stoweidlem37  39591  stoweidlem41  39595  stoweidlem43  39597  stoweidlem44  39598  stoweidlem45  39599  stoweidlem46  39600  stoweidlem48  39602  stoweidlem51  39605  stoweidlem55  39609  stoweidlem59  39613  stoweidlem60  39614  stoweidlem62  39616  fourierdlem2  39663  fourierdlem3  39664  elaa2lem  39787  etransclem11  39799  etransclem24  39812  etransclem26  39814  etransclem28  39816  etransclem35  39823  rrndistlt  39847  ioorrnopn  39862  subsaliuncllem  39912  sge0val  39920  ismea  40005  caragenval  40044  isome  40045  isomenndlem  40081  hoicvrrex  40107  ovnlecvr  40109  ovncvrrp  40115  ovn0lem  40116  ovnsubaddlem1  40121  ovnsubadd  40123  hsphoif  40127  hoidmvval  40128  hsphoival  40130  hoidmvlelem3  40148  hoidmvlelem5  40150  hoidmvle  40151  ovnhoilem1  40152  ovnhoi  40154  ovnlecvr2  40161  ovncvr2  40162  hoidifhspval2  40166  hoiqssbllem2  40174  hspmbllem2  40178  hspmbllem3  40179  hspmbl  40180  ovnovollem1  40207  smfmullem2  40336  smfmul  40339  smfpimcclem  40350  iccpart  40680  iccpartiun  40698  icceuelpart  40700  nnsum3primes4  40995  nnsum3primesgbe  40999  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbnd  41016  isupwlk  41035  ismgmhm  41101  isrnghm  41210  lincval  41516  lincdifsn  41531  linindslinci  41555  lindslinindsimp1  41564  linds0  41572  el0ldep  41573  lindsrng01  41575  snlindsntorlem  41577  ldepspr  41580  islindeps2  41590  zlmodzxzldep  41611  offval0  41617  bigoval  41665  elbigo  41667  setrecseq  41755  aacllem  41880
  Copyright terms: Public domain W3C validator