Theorem fveq1 6872

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 5119	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6512	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6536	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6536	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2794	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5117  ℩cio 6479  ‘cfv 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-ss 3941  df-uni 4882  df-br 5118  df-iota 6481  df-fv 6536

This theorem is referenced by:  fveq1i  6874  fveq1d  6875  iffv  6890  fvmptd3f  6998  fvmptdv2  7001  eqfnun  7024  fsnex  7272  f1prex  7273  isoeq1  7306  oveq  7406  elovmpt3imp  7659  ofrfvalg  7674  offval  7675  offval3  7976  bropopvvv  8084  bropfvvvvlem  8085  poseq  8152  soseq  8153  frrlem1  8280  frrlem13  8292  wfrlem1OLD  8317  wfrlem3OLDa  8320  wfrlem15OLD  8332  smoeq  8359  tfrlem12  8398  tz7.44-2  8416  tz7.44-3  8417  rdgeq1  8420  fsetfocdm  8870  fsetprcnex  8871  mapsncnv  8902  elixp2  8910  resixpfo  8945  elixpsn  8946  mapsnend  9045  enfixsn  9090  mapxpen  9152  ac6sfi  9287  ordtypelem7  9531  wemaplem1  9553  ixpiunwdom  9597  oemapval  9690  cantnf  9700  wemapwe  9704  cnfcom3clem  9712  ssttrcl  9722  ttrcltr  9723  ttrclss  9727  ttrclselem2  9733  updjud  9941  infxpenc2lem2  10027  fseqenlem1  10031  dfac8clem  10039  ac5num  10043  acni  10052  acni2  10053  acnlem  10055  dfac4  10129  dfac5lem5  10134  dfac2a  10137  dfac9  10144  dfacacn  10149  dfac12lem1  10151  dfac12r  10154  cofsmo  10276  cfsmolem  10277  cfsmo  10278  cfcoflem  10279  coftr  10280  alephsing  10283  isfin3ds  10336  fin23lem17  10345  fin23lem32  10351  fin23lem39  10357  isf33lem  10373  isf34lem6  10387  axcc2lem  10443  axcc3  10445  axdc2lem  10455  axdc3lem2  10458  axdc3lem3  10459  axdc3  10461  axdc4lem  10462  axcclem  10464  ac6num  10486  axdclem2  10527  konigthlem  10575  inar1  10782  1fv  13654  axdc4uzlem  13991  seqeq3  14014  seqof  14067  ccatfval  14580  wrdl1s1  14621  ccat1st1st  14635  cshf1  14817  cshweqrep  14828  wrdlen2i  14950  wwlktovf  14964  wwlktovf1  14965  wwlktovfo  14966  wrd2f1tovbij  14968  rtrclreclem1  15065  dfrtrclrec2  15066  rtrclreclem2  15067  rtrclreclem4  15069  dfrtrcl2  15070  clim  15499  rlim  15500  ello1  15520  elo1  15531  summo  15722  fsum  15725  prodmo  15941  fprod  15946  bpolylem  16053  bpolyval  16054  vdwlem6  16993  vdwlem8  16995  ramcl  17036  strfvnd  17191  prdsplusgval  17474  prdsmulrval  17476  prdsleval  17478  prdsdsval  17479  prdsvscaval  17480  xpsff1o  17568  isacs2  17652  isnat  17950  yonedalem3b  18278  yonedainv  18280  ismgmhm  18661  ismhm  18750  prdspjmhm  18794  isgrpinv  18963  pwsmulg  19089  isghm  19185  isghmOLD  19186  cayleylem2  19381  symgfix2  19384  gsmsymgrfix  19396  gsmsymgreq  19400  symgfixelq  19401  pmtr3ncomlem2  19442  pmtrdifel  19448  pmtrdifwrdel  19453  pmtrdifwrdel2  19454  psgnunilem2  19463  psgnunilem3  19464  efgsdm  19698  efgredlemd  19712  efgredlem  19715  efgred  19716  efgrelexlema  19717  efgrelexlemb  19718  prdsgsum  19949  pwspjmhmmgpd  20275  pwsexpg  20276  isrnghm  20388  isabv  20758  islmhm  20972  frgpcyg  21521  psgndiflemB  21547  psgndiflemA  21548  dsmmelbas  21686  frlmipval  21726  frlmphl  21728  uvcf1  21739  islindf  21759  islindf4  21785  psrmulfval  21890  evlslem2  22024  evlslem3  22025  evlslem1  22027  mpfrcl  22030  selvval  22060  psdval  22084  psdcoef  22085  psdadd  22088  psdmul  22091  psdmvr  22094  coe1fval  22128  coe1mul2lem2  22192  coe1tm  22197  madetsumid  22386  mvmulval  22468  marepvval0  22491  mulmarep1gsum2  22499  mdetleib2  22513  m1detdiag  22522  mdetralt  22533  mdetunilem7  22543  mdetunilem9  22545  m2detleiblem3  22554  m2detleiblem4  22555  m2detleib  22556  symgmatr01lem  22578  gsummatr01lem1  22580  gsummatr01lem4  22583  gsummatr01  22584  smadiadetlem3  22593  pmatcoe1fsupp  22626  pmatcollpw3lem  22708  pmatcollpw3fi1lem2  22712  iscnp  23162  1stcfb  23370  ptpjpre1  23496  elpt  23497  elptr  23498  ptpjopn  23537  dfac14  23543  upxp  23548  pthaus  23563  ptrescn  23564  xkoptsub  23579  cnmptkp  23605  xkofvcn  23609  cnmptk1p  23610  cnmptk2  23611  ptunhmeo  23733  ptcmplem3  23979  ptcmplem4  23980  symgtgp  24031  prdstmdd  24049  isucn  24203  imasdsf1olem  24299  prdsxmslem2  24455  tngngp3  24582  nmoval  24641  elcncf  24820  ishtpy  24909  pcoval  24949  om1elbas  24970  elpi1i  24984  iscau  25215  rrxds  25332  rrxdsfival  25352  ehl1eudisval  25360  ehl2eudisval  25362  mbfi1fseqlem6  25660  mbfi1flimlem  25662  isibl  25705  deg1ldg  26036  deg1leb  26039  elply2  26140  elplyr  26145  ne0p  26151  coeeu  26169  coelem  26170  coeeq  26171  coeidlem  26181  elqaalem3  26268  qaa  26270  iaa  26272  aareccl  26273  aannenlem2  26276  aaliou2  26287  dchrptlem2  27214  dchrpt  27216  dchrsum2  27217  sumdchr2  27219  dchrvmaeq0  27453  rpvmasum2  27461  dchrisum0re  27462  ostth  27588  sltval  27597  nolesgn2o  27621  nogesgn1o  27623  noresle  27647  nosupprefixmo  27650  noinfprefixmo  27651  nosupcbv  27652  nosupfv  27656  noinfcbv  27667  noinffv  27671  iscgrg  28425  isismt  28447  israg  28610  iseqlg  28780  brbtwn  28812  brbtwn2  28818  colinearalg  28823  axsegconlem1  28830  axsegcon  28840  ax5seglem5  28846  axpasch  28854  axlowdim  28874  axeuclidlem  28875  axcontlem1  28877  axcontlem2  28878  axcontlem5  28881  vtxdgfval  29381  1egrvtxdg1  29423  isewlk  29516  iswlk  29524  uspgr2wlkeq2  29561  iswlkon  29571  isclwlk  29689  iscrct  29706  iscycl  29707  iswwlks  29752  wwlknon  29773  wlkiswwlks2  29791  wwlksnredwwlkn0  29812  wlksnwwlknvbij  29824  wwlksnextproplem3  29827  wwlksnextprop  29828  umgr2wlk  29865  midwwlks2s3  29868  elwwlks2  29882  elwspths2spth  29883  rusgrnumwwlkslem  29885  rusgrnumwwlkb0  29887  rusgrnumwwlks  29890  isclwwlk  29899  clwlkclwwlklem1  29914  clwwlkn1loopb  29958  clwwlkel  29961  clwwlkf  29962  clwwlkf1  29964  isclwwlknon  30006  clwwlknon1  30012  s2elclwwlknon2  30019  clwwlkvbij  30028  uhgr3cyclex  30097  fusgreg2wsplem  30248  fusgr2wsp2nb  30249  fusgreghash2wsp  30253  2clwwlkel  30264  extwwlkfabel  30268  numclwwlk1lem2fv  30271  numclwwlk1lem2  30275  clwwlknonclwlknonf1o  30277  dlwwlknondlwlknonf1o  30280  numclwwlk2lem1  30291  numclwlk2lem2f  30292  numclwlk2lem2f1o  30294  ex-fv  30358  isnvlem  30525  islno  30668  nmooval  30678  nmblolbi  30715  isphg  30732  ajmoi  30773  ajval  30776  ubthlem3  30787  htthlem  30832  hcau  31099  hlimi  31103  hosmval  31650  hommval  31651  hodmval  31652  hfsmval  31653  hfmmval  31654  adjmo  31747  nmopval  31771  elcnop  31772  ellnop  31773  elunop  31787  elhmop  31788  nmfnval  31791  elcnfn  31797  ellnfn  31798  adjeu  31804  adjval  31805  eigvecval  31811  eigvalfval  31812  adj1  31848  adjeq  31850  hmopadj2  31856  lnopeq0i  31922  lnopeq  31924  elunop2  31928  lnophm  31934  hmopco  31938  nmbdoplb  31940  nmcoplb  31945  lnopcon  31950  lnfn0  31962  lnfnmul  31963  nmbdfnlb  31965  nmcfnlb  31969  lnfncon  31971  riesz4  31979  riesz1  31980  cnlnadjlem9  31990  cnlnadjeu  31993  cnlnssadj  31995  nmopcoi  32010  bra11  32023  cnvbraval  32025  pjss2coi  32079  pjssdif2i  32089  pjssdif1i  32090  pjclem4  32114  pj3si  32122  pj3cor1i  32124  isst  32128  ishst  32129  stri  32172  hstri  32180  aciunf1lem  32574  ismnt  32901  mgcval  32905  ischn  32924  chnind  32929  chnub  32930  fzo0pmtrlast  33040  elrgspnlem1  33174  elrgspnlem2  33175  elrgspnlem3  33176  elrgspnlem4  33177  elrgspn  33178  elrgspnsubrunlem1  33179  linds2eq  33333  elrspunidl  33380  elrspunsn  33381  dfufd2lem  33501  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  fedgmul  33606  fldextrspunlsplem  33649  fldextrspunlsp  33650  fldext2chn  33697  constrextdg2lem  33717  constrextdg2  33718  lmatval  33773  mdetpmtr1  33783  zarcmplem  33841  ismeas  34159  isrnmeas  34160  cntnevol  34188  carsgval  34264  sitgval  34293  eulerpartleme  34324  eulerpartlemd  34327  eulerpartlemr  34335  eulerpartlemgvv  34337  eulerpart  34343  cndprobval  34394  signstfvneq0  34533  reprsum  34574  reprsuc  34576  reprpmtf1o  34587  reprdifc  34588  breprexp  34594  vtsval  34598  hgt750lemb  34617  hgt750lema  34618  hgt750leme  34619  bnj66  34820  bnj106  34828  bnj125  34832  bnj154  34838  bnj155  34839  bnj526  34848  bnj540  34852  bnj609  34877  bnj611  34878  bnj893  34888  bnj1000  34901  bnj1014  34921  bnj1015  34922  bnj1234  34973  bnj1463  35015  gblacfnacd  35059  loop1cycl  35088  derangenlem  35122  subfacp1lem3  35133  subfacp1lem5  35135  subfacp1lem6  35136  subfacp1  35137  sconnpht  35180  cnpconn  35181  txpconn  35183  ptpconn  35184  indispconn  35185  connpconn  35186  cvxpconn  35193  cvmliftmo  35235  cvmliftlem14  35248  cvmliftlem15  35249  cvmliftiota  35252  cvmlift2  35267  cvmliftphtlem  35268  cvmlift3lem2  35271  cvmlift3lem6  35275  cvmlift3lem7  35276  cvmlift3lem9  35278  cvmlift3  35279  satfv1lem  35313  satfv1  35314  sategoelfvb  35370  mrsubff1  35465  mrsub0  35467  mrsubccat  35469  mrsubcn  35470  elmsubrn  35479  msubrn  35480  msubco  35482  msubvrs  35511  mclsax  35520  shftvalg  35678  fwddifval  36109  fwddifnval  36110  bj-evalval  37022  unceq  37550  matunitlindflem2  37570  poimirlem17  37590  poimirlem20  37593  poimirlem22  37595  poimirlem23  37596  poimirlem27  37600  poimirlem28  37601  poimirlem30  37603  poimirlem31  37604  poimirlem32  37605  poimir  37606  broucube  37607  voliunnfl  37617  volsupnfl  37618  itg2addnclem  37624  itg2addnclem3  37626  itg2addnc  37627  ftc1anclem2  37647  ftc1anclem5  37650  upixp  37682  fdc  37698  isismty  37754  rrnmval  37781  elghomlem2OLD  37839  isrngohom  37918  islfl  39007  isopos  39127  islaut  40031  ispautN  40047  isldil  40058  isltrn  40067  ltrnid  40083  ltrneq2  40096  isdilN  40102  istrnN  40105  trlval  40110  ltrneq3  40156  cdleme50ex  40507  cdleme  40508  cdlemg1a  40518  ltrniotaval  40529  ltrniotavalbN  40532  cdlemeiota  40533  cdlemg2jlemOLDN  40541  cdlemg2fvlem  40542  cdlemg2klem  40543  istendo  40708  tendoplcbv  40723  tendopl  40724  tendoicbv  40741  tendoi  40742  tendoid0  40773  tendo1ne0  40776  cdlemksv2  40795  cdlemkuv2  40815  cdlemk33N  40857  cdlemk34  40858  cdlemk36  40861  cdlemk19u  40918  cdlemk  40922  tendoex  40923  dvavsca  40965  dvhvscacbv  41046  dvhvscaval  41047  dicopelval  41125  dicelval1sta  41135  diclspsn  41142  dihmeetlem13N  41267  dih1dimatlem0  41276  dih1dimatlem  41277  dihpN  41284  islpolN  41431  hdmap1fval  41744  hdmapfval  41775  sticksstones1  42088  sticksstones2  42089  sticksstones3  42090  sticksstones8  42095  sticksstones10  42097  sticksstones11  42098  sticksstones12a  42099  sticksstones12  42100  sticksstones15  42103  frlmsnic  42495  uvcn0  42497  pwsgprod  42499  mplmapghm  42511  evlsvval  42515  evlsvvval  42518  evlsvarval  42520  evlsbagval  42521  selvvvval  42540  evlselv  42542  fsuppssindlem2  42547  fsuppssind  42548  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  sn-isghm  42628  ismrc  42656  mzpclval  42680  mzpsubst  42703  mzprename  42704  mzpcompact2lem  42706  eldioph  42713  eldioph2  42717  eldioph2b  42718  eldioph3  42721  rexrabdioph  42749  2rexfrabdioph  42751  3rexfrabdioph  42752  4rexfrabdioph  42753  6rexfrabdioph  42754  7rexfrabdioph  42755  eldioph4i  42767  rabren3dioph  42770  mzpcong  42928  jm2.27dlem1  42965  wepwsolem  42998  aomclem6  43015  aomclem8  43017  dfac11  43018  dgraalem  43101  dgraaub  43104  dgraa0p  43105  mpaaeu  43106  mpaalem  43108  aaitgo  43118  rngunsnply  43125  cantnfresb  43280  tfsconcatun  43293  nvocnvb  43378  eliunov2  43635  rfovcnvfvd  43963  fsovfvd  43966  fsovcnvlem  43969  dssmapfv2d  43974  dssmapnvod  43976  clsk1independent  44002  ntrclskb  44025  ntrclsk13  44027  gneispace2  44088  mnringmulrvald  44184  dvconstbi  44291  addrval  44423  subrval  44424  mulvval  44425  relpeq1  44903  fnchoice  44987  refsum2cnlem1  44995  choicefi  45158  axccdom  45180  fmulcl  45546  fmuldfeqlem1  45547  mccllem  45562  mccl  45563  climf  45587  climf2  45631  dvnprodlem1  45911  dvnprodlem3  45913  dvnprod  45914  stoweidlem2  45967  stoweidlem6  45971  stoweidlem8  45973  stoweidlem9  45974  stoweidlem15  45980  stoweidlem16  45981  stoweidlem17  45982  stoweidlem18  45983  stoweidlem21  45986  stoweidlem27  45992  stoweidlem31  45996  stoweidlem36  46001  stoweidlem37  46002  stoweidlem41  46006  stoweidlem43  46008  stoweidlem44  46009  stoweidlem45  46010  stoweidlem46  46011  stoweidlem48  46013  stoweidlem51  46016  stoweidlem55  46020  stoweidlem59  46024  stoweidlem60  46025  stoweidlem62  46027  fourierdlem2  46074  fourierdlem3  46075  elaa2lem  46198  etransclem11  46210  etransclem24  46223  etransclem26  46225  etransclem28  46227  etransclem35  46234  rrndistlt  46255  ioorrnopn  46270  subsaliuncllem  46322  sge0val  46331  ismea  46416  caragenval  46458  isome  46459  isomenndlem  46495  hoicvrrex  46521  ovnlecvr  46523  ovncvrrp  46529  ovn0lem  46530  ovnsubaddlem1  46535  ovnsubadd  46537  hsphoif  46541  hoidmvval  46542  hsphoival  46544  hoidmvlelem3  46562  hoidmvlelem5  46564  hoidmvle  46565  ovnhoilem1  46566  ovnhoi  46568  ovnlecvr2  46575  ovncvr2  46576  hoidifhspval2  46580  hoiqssbllem2  46588  hspmbllem2  46592  hspmbllem3  46593  hspmbl  46594  ovnovollem1  46621  smfmullem2  46757  smfmul  46760  smfpimcclem  46772  tworepnotupword  46851  cfsetsnfsetfv  47022  cfsetsnfsetfo  47025  iccpart  47356  iccpartiun  47374  icceuelpart  47376  nnsum3primes4  47728  nnsum3primesgbe  47732  nnsum4primesodd  47736  nnsum4primesoddALTV  47737  nnsum4primeseven  47740  nnsum4primesevenALTV  47741  bgoldbtbnd  47749  isisubgr  47801  isgrim  47821  isuspgrim0  47825  grimidvtxedg  47829  grimcnv  47832  grimco  47833  gricushgr  47839  ushggricedg  47849  uhgrimisgrgric  47852  isgrtri  47863  isubgr3stgrlem3  47888  isubgr3stgr  47895  isgrlim  47902  uspgrlim  47912  grlicref  47925  grlicsym  47926  grlictr  47928  isupwlk  48005  lincval  48279  lincdifsn  48294  linindslinci  48318  lindslinindsimp1  48327  linds0  48335  el0ldep  48336  lindsrng01  48338  snlindsntorlem  48340  ldepspr  48343  islindeps2  48353  zlmodzxzldep  48374  bigoval  48423  elbigo  48425  0aryfvalelfv  48509  1arympt1fv  48513  1arymaptfv  48514  1arymaptfo  48517  2arymptfv  48524  2arymaptfv  48525  2arymaptfo  48528  prelrrx2b  48588  rrx2plord  48594  rrx2vlinest  48615  rrx2linesl  48617  elrrx2linest2  48619  line2ylem  48625  line2xlem  48627  itsclc0  48645  itsclc0b  48646  itscnhlinecirc02p  48659  elfvne0  48721  iinfprg  48920  thincciso  49202  thinccisod  49203  setrecseq  49390  aacllem  49506