Theorem fveq1 6839

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.

Step	Hyp	Ref	Expression
1		breq 5104	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6483	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6507	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6507	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102  ℩cio 6450  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  fveq1i  6841  fveq1d  6842  iffv  6857  fvmptd3f  6965  fvmptdv2  6968  eqfnun  6991  fsnex  7240  f1prex  7241  isoeq1  7274  oveq  7375  elovmpt3imp  7626  ofrfvalg  7641  offval  7642  offval3  7940  bropopvvv  8046  bropfvvvvlem  8047  poseq  8114  soseq  8115  frrlem1  8242  frrlem13  8254  smoeq  8296  tfrlem12  8334  tz7.44-2  8352  tz7.44-3  8353  rdgeq1  8356  fsetfocdm  8811  fsetprcnex  8812  mapsncnv  8843  elixp2  8851  resixpfo  8886  elixpsn  8887  mapsnend  8984  enfixsn  9027  mapxpen  9084  ac6sfi  9207  ordtypelem7  9453  wemaplem1  9475  ixpiunwdom  9519  oemapval  9612  cantnf  9622  wemapwe  9626  cnfcom3clem  9634  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  updjud  9863  infxpenc2lem2  9949  fseqenlem1  9953  dfac8clem  9961  ac5num  9965  acni  9974  acni2  9975  acnlem  9977  dfac4  10051  dfac5lem5  10056  dfac2a  10059  dfac9  10066  dfacacn  10071  dfac12lem1  10073  dfac12r  10076  cofsmo  10198  cfsmolem  10199  cfsmo  10200  cfcoflem  10201  coftr  10202  alephsing  10205  isfin3ds  10258  fin23lem17  10267  fin23lem32  10273  fin23lem39  10279  isf33lem  10295  isf34lem6  10309  axcc2lem  10365  axcc3  10367  axdc2lem  10377  axdc3lem2  10380  axdc3lem3  10381  axdc3  10383  axdc4lem  10384  axcclem  10386  ac6num  10408  axdclem2  10449  konigthlem  10497  inar1  10704  1fv  13584  axdc4uzlem  13924  seqeq3  13947  seqof  14000  ccatfval  14514  wrdl1s1  14555  ccat1st1st  14569  cshf1  14751  cshweqrep  14762  wrdlen2i  14884  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  wrd2f1tovbij  14902  rtrclreclem1  14999  dfrtrclrec2  15000  rtrclreclem2  15001  rtrclreclem4  15003  dfrtrcl2  15004  clim  15436  rlim  15437  ello1  15457  elo1  15468  summo  15659  fsum  15662  prodmo  15878  fprod  15883  bpolylem  15990  bpolyval  15991  vdwlem6  16933  vdwlem8  16935  ramcl  16976  strfvnd  17131  prdsplusgval  17412  prdsmulrval  17414  prdsleval  17416  prdsdsval  17417  prdsvscaval  17418  xpsff1o  17506  isacs2  17594  isnat  17892  yonedalem3b  18220  yonedainv  18222  ismgmhm  18605  ismhm  18694  prdspjmhm  18738  isgrpinv  18907  pwsmulg  19033  isghm  19129  isghmOLD  19130  cayleylem2  19327  symgfix2  19330  gsmsymgrfix  19342  gsmsymgreq  19346  symgfixelq  19347  pmtr3ncomlem2  19388  pmtrdifel  19394  pmtrdifwrdel  19399  pmtrdifwrdel2  19400  psgnunilem2  19409  psgnunilem3  19410  efgsdm  19644  efgredlemd  19658  efgredlem  19661  efgred  19662  efgrelexlema  19663  efgrelexlemb  19664  prdsgsum  19895  pwspjmhmmgpd  20248  pwsexpg  20249  isrnghm  20361  isabv  20731  islmhm  20966  frgpcyg  21515  psgndiflemB  21542  psgndiflemA  21543  dsmmelbas  21681  frlmipval  21721  frlmphl  21723  uvcf1  21734  islindf  21754  islindf4  21780  psrmulfval  21885  evlslem2  22019  evlslem3  22020  evlslem1  22022  mpfrcl  22025  selvval  22055  psdval  22079  psdcoef  22080  psdadd  22083  psdmul  22086  psdmvr  22089  coe1fval  22123  coe1mul2lem2  22187  coe1tm  22192  madetsumid  22381  mvmulval  22463  marepvval0  22486  mulmarep1gsum2  22494  mdetleib2  22508  m1detdiag  22517  mdetralt  22528  mdetunilem7  22538  mdetunilem9  22540  m2detleiblem3  22549  m2detleiblem4  22550  m2detleib  22551  symgmatr01lem  22573  gsummatr01lem1  22575  gsummatr01lem4  22578  gsummatr01  22579  smadiadetlem3  22588  pmatcoe1fsupp  22621  pmatcollpw3lem  22703  pmatcollpw3fi1lem2  22707  iscnp  23157  1stcfb  23365  ptpjpre1  23491  elpt  23492  elptr  23493  ptpjopn  23532  dfac14  23538  upxp  23543  pthaus  23558  ptrescn  23559  xkoptsub  23574  cnmptkp  23600  xkofvcn  23604  cnmptk1p  23605  cnmptk2  23606  ptunhmeo  23728  ptcmplem3  23974  ptcmplem4  23975  symgtgp  24026  prdstmdd  24044  isucn  24198  imasdsf1olem  24294  prdsxmslem2  24450  tngngp3  24577  nmoval  24636  elcncf  24815  ishtpy  24904  pcoval  24944  om1elbas  24965  elpi1i  24979  iscau  25209  rrxds  25326  rrxdsfival  25346  ehl1eudisval  25354  ehl2eudisval  25356  mbfi1fseqlem6  25654  mbfi1flimlem  25656  isibl  25699  deg1ldg  26030  deg1leb  26033  elply2  26134  elplyr  26139  ne0p  26145  coeeu  26163  coelem  26164  coeeq  26165  coeidlem  26175  elqaalem3  26262  qaa  26264  iaa  26266  aareccl  26267  aannenlem2  26270  aaliou2  26281  dchrptlem2  27209  dchrpt  27211  dchrsum2  27212  sumdchr2  27214  dchrvmaeq0  27448  rpvmasum2  27456  dchrisum0re  27457  ostth  27583  sltval  27592  nolesgn2o  27616  nogesgn1o  27618  noresle  27642  nosupprefixmo  27645  noinfprefixmo  27646  nosupcbv  27647  nosupfv  27651  noinfcbv  27662  noinffv  27666  iscgrg  28492  isismt  28514  israg  28677  iseqlg  28847  brbtwn  28879  brbtwn2  28885  colinearalg  28890  axsegconlem1  28897  axsegcon  28907  ax5seglem5  28913  axpasch  28921  axlowdim  28941  axeuclidlem  28942  axcontlem1  28944  axcontlem2  28945  axcontlem5  28948  vtxdgfval  29448  1egrvtxdg1  29490  isewlk  29583  iswlk  29591  uspgr2wlkeq2  29627  iswlkon  29636  isclwlk  29753  iscrct  29770  iscycl  29771  iswwlks  29816  wwlknon  29837  wlkiswwlks2  29855  wwlksnredwwlkn0  29876  wlksnwwlknvbij  29888  wwlksnextproplem3  29891  wwlksnextprop  29892  umgr2wlk  29929  midwwlks2s3  29932  elwwlks2  29946  elwspths2spth  29947  rusgrnumwwlkslem  29949  rusgrnumwwlkb0  29951  rusgrnumwwlks  29954  isclwwlk  29963  clwlkclwwlklem1  29978  clwwlkn1loopb  30022  clwwlkel  30025  clwwlkf  30026  clwwlkf1  30028  isclwwlknon  30070  clwwlknon1  30076  s2elclwwlknon2  30083  clwwlkvbij  30092  uhgr3cyclex  30161  fusgreg2wsplem  30312  fusgr2wsp2nb  30313  fusgreghash2wsp  30317  2clwwlkel  30328  extwwlkfabel  30332  numclwwlk1lem2fv  30335  numclwwlk1lem2  30339  clwwlknonclwlknonf1o  30341  dlwwlknondlwlknonf1o  30344  numclwwlk2lem1  30355  numclwlk2lem2f  30356  numclwlk2lem2f1o  30358  ex-fv  30422  isnvlem  30589  islno  30732  nmooval  30742  nmblolbi  30779  isphg  30796  ajmoi  30837  ajval  30840  ubthlem3  30851  htthlem  30896  hcau  31163  hlimi  31167  hosmval  31714  hommval  31715  hodmval  31716  hfsmval  31717  hfmmval  31718  adjmo  31811  nmopval  31835  elcnop  31836  ellnop  31837  elunop  31851  elhmop  31852  nmfnval  31855  elcnfn  31861  ellnfn  31862  adjeu  31868  adjval  31869  eigvecval  31875  eigvalfval  31876  adj1  31912  adjeq  31914  hmopadj2  31920  lnopeq0i  31986  lnopeq  31988  elunop2  31992  lnophm  31998  hmopco  32002  nmbdoplb  32004  nmcoplb  32009  lnopcon  32014  lnfn0  32026  lnfnmul  32027  nmbdfnlb  32029  nmcfnlb  32033  lnfncon  32035  riesz4  32043  riesz1  32044  cnlnadjlem9  32054  cnlnadjeu  32057  cnlnssadj  32059  nmopcoi  32074  bra11  32087  cnvbraval  32089  pjss2coi  32143  pjssdif2i  32153  pjssdif1i  32154  pjclem4  32178  pj3si  32186  pj3cor1i  32188  isst  32192  ishst  32193  stri  32236  hstri  32244  aciunf1lem  32636  ismnt  32955  mgcval  32959  ischn  32978  chnind  32983  chnub  32984  fzo0pmtrlast  33064  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspn  33213  elrgspnsubrunlem1  33214  linds2eq  33345  elrspunidl  33392  elrspunsn  33393  dfufd2lem  33513  lbsdiflsp0  33615  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  fldextrspunlsplem  33661  fldextrspunlsp  33662  fldext2chn  33711  constrextdg2lem  33731  constrextdg2  33732  lmatval  33796  mdetpmtr1  33806  zarcmplem  33864  ismeas  34182  isrnmeas  34183  cntnevol  34211  carsgval  34287  sitgval  34316  eulerpartleme  34347  eulerpartlemd  34350  eulerpartlemr  34358  eulerpartlemgvv  34360  eulerpart  34366  cndprobval  34417  signstfvneq0  34556  reprsum  34597  reprsuc  34599  reprpmtf1o  34610  reprdifc  34611  breprexp  34617  vtsval  34621  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  bnj66  34843  bnj106  34851  bnj125  34855  bnj154  34861  bnj155  34862  bnj526  34871  bnj540  34875  bnj609  34900  bnj611  34901  bnj893  34911  bnj1000  34924  bnj1014  34944  bnj1015  34945  bnj1234  34996  bnj1463  35038  gblacfnacd  35082  loop1cycl  35117  derangenlem  35151  subfacp1lem3  35162  subfacp1lem5  35164  subfacp1lem6  35165  subfacp1  35166  sconnpht  35209  cnpconn  35210  txpconn  35212  ptpconn  35213  indispconn  35214  connpconn  35215  cvxpconn  35222  cvmliftmo  35264  cvmliftlem14  35277  cvmliftlem15  35278  cvmliftiota  35281  cvmlift2  35296  cvmliftphtlem  35297  cvmlift3lem2  35300  cvmlift3lem6  35304  cvmlift3lem7  35305  cvmlift3lem9  35307  cvmlift3  35308  satfv1lem  35342  satfv1  35343  sategoelfvb  35399  mrsubff1  35494  mrsub0  35496  mrsubccat  35498  mrsubcn  35499  elmsubrn  35508  msubrn  35509  msubco  35511  msubvrs  35540  mclsax  35549  shftvalg  35712  fwddifval  36143  fwddifnval  36144  bj-evalval  37056  unceq  37584  matunitlindflem2  37604  poimirlem17  37624  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  poimirlem27  37634  poimirlem28  37635  poimirlem30  37637  poimirlem31  37638  poimirlem32  37639  poimir  37640  broucube  37641  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  ftc1anclem2  37681  ftc1anclem5  37684  upixp  37716  fdc  37732  isismty  37788  rrnmval  37815  elghomlem2OLD  37873  isrngohom  37952  islfl  39046  isopos  39166  islaut  40070  ispautN  40086  isldil  40097  isltrn  40106  ltrnid  40122  ltrneq2  40135  isdilN  40141  istrnN  40144  trlval  40149  ltrneq3  40195  cdleme50ex  40546  cdleme  40547  cdlemg1a  40557  ltrniotaval  40568  ltrniotavalbN  40571  cdlemeiota  40572  cdlemg2jlemOLDN  40580  cdlemg2fvlem  40581  cdlemg2klem  40582  istendo  40747  tendoplcbv  40762  tendopl  40763  tendoicbv  40780  tendoi  40781  tendoid0  40812  tendo1ne0  40815  cdlemksv2  40834  cdlemkuv2  40854  cdlemk33N  40896  cdlemk34  40897  cdlemk36  40900  cdlemk19u  40957  cdlemk  40961  tendoex  40962  dvavsca  41004  dvhvscacbv  41085  dvhvscaval  41086  dicopelval  41164  dicelval1sta  41174  diclspsn  41181  dihmeetlem13N  41306  dih1dimatlem0  41315  dih1dimatlem  41316  dihpN  41323  islpolN  41470  hdmap1fval  41783  hdmapfval  41814  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones15  42142  frlmsnic  42521  uvcn0  42523  pwsgprod  42525  mplmapghm  42537  evlsvval  42541  evlsvvval  42544  evlsvarval  42546  evlsbagval  42547  selvvvval  42566  evlselv  42568  fsuppssindlem2  42573  fsuppssind  42574  prjspnfv01  42605  prjspner01  42606  prjspner1  42607  sn-isghm  42654  ismrc  42682  mzpclval  42706  mzpsubst  42729  mzprename  42730  mzpcompact2lem  42732  eldioph  42739  eldioph2  42743  eldioph2b  42744  eldioph3  42747  rexrabdioph  42775  2rexfrabdioph  42777  3rexfrabdioph  42778  4rexfrabdioph  42779  6rexfrabdioph  42780  7rexfrabdioph  42781  eldioph4i  42793  rabren3dioph  42796  mzpcong  42954  jm2.27dlem1  42991  wepwsolem  43024  aomclem6  43041  aomclem8  43043  dfac11  43044  dgraalem  43127  dgraaub  43130  dgraa0p  43131  mpaaeu  43132  mpaalem  43134  aaitgo  43144  rngunsnply  43151  cantnfresb  43306  tfsconcatun  43319  nvocnvb  43404  eliunov2  43661  rfovcnvfvd  43989  fsovfvd  43992  fsovcnvlem  43995  dssmapfv2d  44000  dssmapnvod  44002  clsk1independent  44028  ntrclskb  44051  ntrclsk13  44053  gneispace2  44114  mnringmulrvald  44209  dvconstbi  44316  addrval  44448  subrval  44449  mulvval  44450  relpeq1  44927  fnchoice  45016  refsum2cnlem1  45024  choicefi  45187  axccdom  45209  fmulcl  45572  fmuldfeqlem1  45573  mccllem  45588  mccl  45589  climf  45613  climf2  45657  dvnprodlem1  45937  dvnprodlem3  45939  dvnprod  45940  stoweidlem2  45993  stoweidlem6  45997  stoweidlem8  45999  stoweidlem9  46000  stoweidlem15  46006  stoweidlem16  46007  stoweidlem17  46008  stoweidlem18  46009  stoweidlem21  46012  stoweidlem27  46018  stoweidlem31  46022  stoweidlem36  46027  stoweidlem37  46028  stoweidlem41  46032  stoweidlem43  46034  stoweidlem44  46035  stoweidlem45  46036  stoweidlem46  46037  stoweidlem48  46039  stoweidlem51  46042  stoweidlem55  46046  stoweidlem59  46050  stoweidlem60  46051  stoweidlem62  46053  fourierdlem2  46100  fourierdlem3  46101  elaa2lem  46224  etransclem11  46236  etransclem24  46249  etransclem26  46251  etransclem28  46253  etransclem35  46260  rrndistlt  46281  ioorrnopn  46296  subsaliuncllem  46348  sge0val  46357  ismea  46442  caragenval  46484  isome  46485  isomenndlem  46521  hoicvrrex  46547  ovnlecvr  46549  ovncvrrp  46555  ovn0lem  46556  ovnsubaddlem1  46561  ovnsubadd  46563  hsphoif  46567  hoidmvval  46568  hsphoival  46570  hoidmvlelem3  46588  hoidmvlelem5  46590  hoidmvle  46591  ovnhoilem1  46592  ovnhoi  46594  ovnlecvr2  46601  ovncvr2  46602  hoidifhspval2  46606  hoiqssbllem2  46614  hspmbllem2  46618  hspmbllem3  46619  hspmbl  46620  ovnovollem1  46647  smfmullem2  46783  smfmul  46786  smfpimcclem  46798  tworepnotupword  46877  sinnpoly  46885  cfsetsnfsetfv  47051  cfsetsnfsetfo  47054  iccpart  47410  iccpartiun  47428  icceuelpart  47430  nnsum3primes4  47782  nnsum3primesgbe  47786  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbnd  47803  isisubgr  47855  isgrim  47875  grimidvtxedg  47878  grimcnv  47881  grimco  47882  isuspgrim0  47887  gricushgr  47910  ushggricedg  47920  uhgrimisgrgric  47924  isgrtri  47935  isubgr3stgrlem3  47960  isubgr3stgr  47967  isgrlim  47974  uspgrlim  47984  grlicref  47997  grlicsym  47998  grlictr  48000  isupwlk  48117  lincval  48391  lincdifsn  48406  linindslinci  48430  lindslinindsimp1  48439  linds0  48447  el0ldep  48448  lindsrng01  48450  snlindsntorlem  48452  ldepspr  48455  islindeps2  48465  zlmodzxzldep  48486  bigoval  48531  elbigo  48533  0aryfvalelfv  48617  1arympt1fv  48621  1arymaptfv  48622  1arymaptfo  48625  2arymptfv  48632  2arymaptfv  48633  2arymaptfo  48636  prelrrx2b  48696  rrx2plord  48702  rrx2vlinest  48723  rrx2linesl  48725  elrrx2linest2  48727  line2ylem  48733  line2xlem  48735  itsclc0  48753  itsclc0b  48754  itscnhlinecirc02p  48767  elfvne0  48830  iinfprg  49041  thincciso  49435  thinccisod  49436  setrecseq  49667  aacllem  49783