Theorem fveq1 6866

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 5102	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6505	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6529	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6529	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2822	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1560   class class class wbr 5100  ℩cio 6475  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529

This theorem is referenced by:  fveq1i  6868  fveq1d  6869  iffv  6884  fvmptd3f  6991  fvmptdv2  6994  eqfnun  7018  fsnex  7267  f1prex  7268  isoeq1  7301  oveq  7402  elovmpt3imp  7653  ofrfvalg  7668  offval  7669  offval3  7963  bropopvvv  8069  bropfvvvvlem  8070  poseq  8138  soseq  8139  frrlem1  8267  frrlem13  8279  smoeq  8321  tfrlem12  8360  tz7.44-2  8378  tz7.44-3  8379  rdgeq1  8382  fsetfocdm  8842  fsetprcnex  8843  mapsncnv  8875  elixp2  8883  resixpfo  8918  elixpsn  8919  mapsnend  9017  enfixsn  9058  mapxpen  9115  ac6sfi  9228  ordtypelem7  9472  wemaplem1  9494  ixpiunwdom  9538  oemapval  9638  cantnf  9648  wemapwe  9652  cnfcom3clem  9660  ssttrcl  9670  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  updjud  9892  infxpenc2lem2  9976  fseqenlem1  9980  dfac8clem  9988  ac5num  9992  acni  10001  acni2  10002  acnlem  10004  dfac4  10078  dfac5lem5  10083  dfac2a  10086  dfac9  10093  dfacacn  10098  dfac12lem1  10100  dfac12r  10103  cofsmo  10226  cfsmolem  10227  cfsmo  10228  cfcoflem  10229  coftr  10230  alephsing  10233  isfin3ds  10286  fin23lem17  10295  fin23lem32  10301  fin23lem39  10307  isf33lem  10323  isf34lem6  10337  axcc2lem  10393  axcc3  10395  axdc2lem  10405  axdc3lem2  10408  axdc3lem3  10409  axdc3  10411  axdc4lem  10412  axcclem  10414  ac6num  10436  axdclem2  10477  konigthlem  10526  inar1  10733  1fv  13652  axdc4uzlem  13996  seqeq3  14019  seqof  14072  ccatfval  14586  wrdl1s1  14628  ccat1st1st  14642  cshf1  14823  cshweqrep  14834  wrdlen2i  14955  wwlktovf  14969  wwlktovf1  14970  wwlktovfo  14971  wrd2f1tovbij  14973  rtrclreclem1  15070  dfrtrclrec2  15071  rtrclreclem2  15072  rtrclreclem4  15074  dfrtrcl2  15075  clim  15521  rlim  15522  ello1  15542  elo1  15553  summo  15744  fsum  15747  prodmo  15966  fprod  15971  bpolylem  16078  bpolyval  16079  vdwlem6  17022  vdwlem8  17024  ramcl  17065  strfvnd  17221  prdsplusgval  17502  prdsmulrval  17504  prdsleval  17506  prdsdsval  17507  prdsvscaval  17508  xpsff1o  17597  isacs2  17685  isnat  17983  yonedalem3b  18311  yonedainv  18313  ischn  18639  chnind  18653  chnub  18654  ismgmhm  18730  ismhm  18819  prdspjmhm  18863  isgrpinv  19035  pwsmulg  19161  isghm  19256  cayleylem2  19453  symgfix2  19456  gsmsymgrfix  19468  gsmsymgreq  19472  symgfixelq  19473  pmtr3ncomlem2  19514  pmtrdifel  19520  pmtrdifwrdel  19525  pmtrdifwrdel2  19526  psgnunilem2  19535  psgnunilem3  19536  efgsdm  19770  efgredlemd  19784  efgredlem  19787  efgred  19788  efgrelexlema  19789  efgrelexlemb  19790  prdsgsum  20021  pwspjmhmmgpd  20372  pwsexpg  20373  pwsgprod  20374  isrnghm  20486  isabv  20857  islmhm  21091  frgpcyg  21622  psgndiflemB  21649  psgndiflemA  21650  dsmmelbas  21788  frlmipval  21828  frlmphl  21830  uvcf1  21841  islindf  21861  islindf4  21887  psrmulfval  21992  evlslem2  22129  evlslem3  22130  evlslem1  22132  mpfrcl  22135  evlsvval  22140  evlsvvval  22143  selvval  22170  mplmapghm  22172  evlsvarval  22177  selvvvval  22192  psdval  22221  psdcoef  22222  psdadd  22225  psdmul  22228  psdmvr  22231  coe1fval  22264  coe1mul2lem2  22328  coe1tm  22333  madetsumid  22518  mvmulval  22600  marepvval0  22623  mulmarep1gsum2  22631  mdetleib2  22645  m1detdiag  22654  mdetralt  22665  mdetunilem7  22675  mdetunilem9  22677  m2detleiblem3  22686  m2detleiblem4  22687  m2detleib  22688  symgmatr01lem  22710  gsummatr01lem1  22712  gsummatr01lem4  22715  gsummatr01  22716  smadiadetlem3  22725  pmatcoe1fsupp  22758  pmatcollpw3lem  22840  pmatcollpw3fi1lem2  22844  iscnp  23294  1stcfb  23502  ptpjpre1  23628  elpt  23629  elptr  23630  ptpjopn  23669  dfac14  23675  upxp  23680  pthaus  23695  ptrescn  23696  xkoptsub  23711  cnmptkp  23737  xkofvcn  23741  cnmptk1p  23742  cnmptk2  23743  ptunhmeo  23865  ptcmplem3  24111  ptcmplem4  24112  symgtgp  24163  prdstmdd  24181  isucn  24334  imasdsf1olem  24430  prdsxmslem2  24586  tngngp3  24713  nmoval  24772  elcncf  24948  ishtpy  25031  pcoval  25070  om1elbas  25091  elpi1i  25105  iscau  25335  rrxds  25452  rrxdsfival  25472  ehl1eudisval  25480  ehl2eudisval  25482  mbfi1fseqlem6  25779  mbfi1flimlem  25781  isibl  25824  deg1ldg  26149  deg1leb  26152  elply2  26253  elplyr  26258  ne0p  26264  coeeu  26282  coelem  26283  coeeq  26284  coeidlem  26294  elqaalem3  26382  qaa  26384  iaa  26386  aareccl  26387  aannenlem2  26390  aaliou2  26401  dchrptlem2  27326  dchrpt  27328  dchrsum2  27329  sumdchr2  27331  dchrvmaeq0  27565  rpvmasum2  27573  dchrisum0re  27574  ostth  27700  ltsval  27708  nolesgn2o  27732  nogesgn1o  27734  noresle  27758  nosupprefixmo  27761  noinfprefixmo  27762  nosupcbv  27763  nosupfv  27767  noinfcbv  27778  noinffv  27782  iscgrg  28678  isismt  28700  israg  28867  iseqlg  29058  brbtwn  29097  brbtwn2  29103  colinearalg  29108  axsegconlem1  29115  axsegcon  29125  ax5seglem5  29131  axpasch  29139  axlowdim  29159  axeuclidlem  29160  axcontlem1  29162  axcontlem2  29163  axcontlem5  29166  vtxdgfval  29665  1egrvtxdg1  29707  isewlk  29800  iswlk  29808  uspgr2wlkeq2  29844  iswlkon  29853  isclwlk  29970  iscrct  29987  iscycl  29988  iswwlks  30033  wwlknon  30054  wlkiswwlks2  30072  wwlksnredwwlkn0  30093  wlksnwwlknvbij  30105  wwlksnextproplem3  30108  wwlksnextprop  30109  umgr2wlk  30146  midwwlks2s3  30149  elwwlks2  30166  elwspths2spth  30167  rusgrnumwwlkslem  30169  rusgrnumwwlkb0  30171  rusgrnumwwlks  30174  isclwwlk  30183  clwlkclwwlklem1  30198  clwwlkn1loopb  30242  clwwlkel  30245  clwwlkf  30246  clwwlkf1  30248  isclwwlknon  30290  clwwlknon1  30296  s2elclwwlknon2  30303  clwwlkvbij  30312  uhgr3cyclex  30381  fusgreg2wsplem  30532  fusgr2wsp2nb  30533  fusgreghash2wsp  30537  2clwwlkel  30548  extwwlkfabel  30552  numclwwlk1lem2fv  30555  numclwwlk1lem2  30559  clwwlknonclwlknonf1o  30561  dlwwlknondlwlknonf1o  30564  numclwwlk2lem1  30575  numclwlk2lem2f  30576  numclwlk2lem2f1o  30578  ex-fv  30642  isnvlem  30810  islno  30953  nmooval  30963  nmblolbi  31000  isphg  31017  ajmoi  31058  ajval  31061  ubthlem3  31072  htthlem  31117  hcau  31384  hlimi  31388  hosmval  31935  hommval  31936  hodmval  31937  hfsmval  31938  hfmmval  31939  adjmo  32032  nmopval  32056  elcnop  32057  ellnop  32058  elunop  32072  elhmop  32073  nmfnval  32076  elcnfn  32082  ellnfn  32083  adjeu  32089  adjval  32090  eigvecval  32096  eigvalfval  32097  adj1  32133  adjeq  32135  hmopadj2  32141  lnopeq0i  32207  lnopeq  32209  elunop2  32213  lnophm  32219  hmopco  32223  nmbdoplb  32225  nmcoplb  32230  lnopcon  32235  lnfn0  32247  lnfnmul  32248  nmbdfnlb  32250  nmcfnlb  32254  lnfncon  32256  riesz4  32264  riesz1  32265  cnlnadjlem9  32275  cnlnadjeu  32278  cnlnssadj  32280  nmopcoi  32295  bra11  32308  cnvbraval  32310  pjss2coi  32364  pjssdif2i  32374  pjssdif1i  32375  pjclem4  32399  pj3si  32407  pj3cor1i  32409  isst  32413  ishst  32414  stri  32457  hstri  32465  aciunf1lem  32861  ismnt  33158  mgcval  33162  fzo0pmtrlast  33269  elrgspnlem1  33420  elrgspnlem2  33421  elrgspnlem3  33422  elrgspnlem4  33423  elrgspn  33424  elrgspnsubrunlem1  33425  linds2eq  33564  elrspunidl  33611  elrspunsn  33612  dfufd2lem  33742  psrnzr  33806  0mplrim  33808  0mplric  33809  selvply1rhmlema  33812  selvply1rhmlemb  33813  selvply1rhmlem1  33814  selvply1rhmlem3  33816  selvply1rhmlem5  33818  selvply1rhm  33819  mplidom  33822  extvfv  33827  extvfvv  33828  extvfvcl  33830  evlvarval  33835  evlextv  33836  mplvrpmga  33839  splysubrg  33854  issply  33855  vietalem  33873  vieta  33874  lbsdiflsp0  33920  fedgmullem1  33923  fedgmullem2  33924  fedgmul  33925  fldextrspunlsplem  33967  fldextrspunlsp  33968  fldext2chn  34022  constrextdg2lem  34042  constrextdg2  34043  lmatval  34107  mdetpmtr1  34117  zarcmplem  34175  ismeas  34493  isrnmeas  34494  cntnevol  34522  carsgval  34597  sitgval  34626  eulerpartleme  34657  eulerpartlemd  34660  eulerpartlemr  34668  eulerpartlemgvv  34670  eulerpart  34676  cndprobval  34727  signstfvneq0  34863  reprsum  34904  reprsuc  34906  reprpmtf1o  34917  reprdifc  34918  breprexp  34924  vtsval  34928  hgt750lemb  34947  hgt750lema  34948  hgt750leme  34949  bnj66  35152  bnj106  35160  bnj125  35164  bnj154  35170  bnj155  35171  bnj526  35180  bnj540  35184  bnj609  35209  bnj611  35210  bnj893  35220  bnj1000  35233  bnj1014  35253  bnj1015  35254  bnj1234  35305  bnj1463  35347  fineqvnttrclse  35417  gblacfnacd  35442  loop1cycl  35484  derangenlem  35518  subfacp1lem3  35529  subfacp1lem5  35531  subfacp1lem6  35532  subfacp1  35533  sconnpht  35576  cnpconn  35577  txpconn  35579  ptpconn  35580  indispconn  35581  connpconn  35582  cvxpconn  35589  cvmliftmo  35631  cvmliftlem14  35644  cvmliftlem15  35645  cvmliftiota  35648  cvmlift2  35663  cvmliftphtlem  35664  cvmlift3lem2  35667  cvmlift3lem6  35671  cvmlift3lem7  35672  cvmlift3lem9  35674  cvmlift3  35675  satfv1lem  35709  satfv1  35710  sategoelfvb  35766  mrsubff1  35861  mrsub0  35863  mrsubccat  35865  mrsubcn  35866  elmsubrn  35875  msubrn  35876  msubco  35878  msubvrs  35907  mclsax  35916  shftvalg  36079  fwddifval  36509  fwddifnval  36510  bj-evalval  37562  unceq  38093  matunitlindflem2  38113  poimirlem17  38133  poimirlem20  38136  poimirlem22  38138  poimirlem23  38139  poimirlem27  38143  poimirlem28  38144  poimirlem30  38146  poimirlem31  38147  poimirlem32  38148  poimir  38149  broucube  38150  voliunnfl  38160  volsupnfl  38161  itg2addnclem  38167  itg2addnclem3  38169  itg2addnc  38170  ftc1anclem2  38190  ftc1anclem5  38193  upixp  38225  fdc  38241  isismty  38297  rrnmval  38324  elghomlem2OLD  38382  isrngohom  38461  islfl  39681  isopos  39801  islaut  40704  ispautN  40720  isldil  40731  isltrn  40740  ltrnid  40756  ltrneq2  40769  isdilN  40775  istrnN  40778  trlval  40783  ltrneq3  40829  cdleme50ex  41180  cdleme  41181  cdlemg1a  41191  ltrniotaval  41202  ltrniotavalbN  41205  cdlemeiota  41206  cdlemg2jlemOLDN  41214  cdlemg2fvlem  41215  cdlemg2klem  41216  istendo  41381  tendoplcbv  41396  tendopl  41397  tendoicbv  41414  tendoi  41415  tendoid0  41446  tendo1ne0  41449  cdlemksv2  41468  cdlemkuv2  41488  cdlemk33N  41530  cdlemk34  41531  cdlemk36  41534  cdlemk19u  41591  cdlemk  41595  tendoex  41596  dvavsca  41638  dvhvscacbv  41719  dvhvscaval  41720  dicopelval  41798  dicelval1sta  41808  diclspsn  41815  dihmeetlem13N  41940  dih1dimatlem0  41949  dih1dimatlem  41950  dihpN  41957  islpolN  42104  hdmap1fval  42417  hdmapfval  42448  sticksstones1  42760  sticksstones2  42761  sticksstones3  42762  sticksstones8  42767  sticksstones10  42769  sticksstones11  42770  sticksstones12a  42771  sticksstones12  42772  sticksstones15  42775  frlmsnic  43155  uvcn0  43157  evlsbagval  43165  evlselv  43168  fsuppssindlem2  43171  fsuppssind  43172  prjspnfv01  43203  prjspner01  43204  prjspner1  43205  sn-isghm  43252  ismrc  43279  mzpclval  43303  mzpsubst  43326  mzprename  43327  mzpcompact2lem  43329  eldioph  43336  eldioph2  43340  eldioph2b  43341  eldioph3  43344  rexrabdioph  43368  2rexfrabdioph  43370  3rexfrabdioph  43371  4rexfrabdioph  43372  6rexfrabdioph  43373  7rexfrabdioph  43374  eldioph4i  43386  rabren3dioph  43389  mzpcong  43546  jm2.27dlem1  43583  wepwsolem  43616  aomclem6  43633  aomclem8  43635  dfac11  43636  dgraalem  43719  dgraaub  43722  dgraa0p  43723  mpaaeu  43724  mpaalem  43726  aaitgo  43736  rngunsnply  43743  cantnfresb  43898  tfsconcatun  43911  nvocnvb  43995  eliunov2  44252  rfovcnvfvd  44580  fsovfvd  44583  fsovcnvlem  44586  dssmapfv2d  44591  dssmapnvod  44593  clsk1independent  44619  ntrclskb  44642  ntrclsk13  44644  gneispace2  44705  mnringmulrvald  44800  dvconstbi  44907  addrval  45038  subrval  45039  mulvval  45040  relpeq1  45517  fnchoice  45606  refsum2cnlem1  45614  choicefi  45774  axccdom  45795  fmulcl  46154  fmuldfeqlem1  46155  mccllem  46170  mccl  46171  climf  46195  climf2  46237  dvnprodlem1  46517  dvnprodlem3  46519  dvnprod  46520  stoweidlem2  46573  stoweidlem6  46577  stoweidlem8  46579  stoweidlem9  46580  stoweidlem15  46586  stoweidlem16  46587  stoweidlem17  46588  stoweidlem18  46589  stoweidlem21  46592  stoweidlem27  46598  stoweidlem31  46602  stoweidlem36  46607  stoweidlem37  46608  stoweidlem41  46612  stoweidlem43  46614  stoweidlem44  46615  stoweidlem45  46616  stoweidlem46  46617  stoweidlem48  46619  stoweidlem51  46622  stoweidlem55  46626  stoweidlem59  46630  stoweidlem60  46631  stoweidlem62  46633  fourierdlem2  46680  fourierdlem3  46681  elaa2lem  46804  etransclem11  46816  etransclem24  46829  etransclem26  46831  etransclem28  46833  etransclem35  46840  rrndistlt  46861  ioorrnopn  46876  subsaliuncllem  46928  sge0val  46937  ismea  47022  caragenval  47064  isome  47065  isomenndlem  47101  hoicvrrex  47127  ovnlecvr  47129  ovncvrrp  47135  ovn0lem  47136  ovnsubaddlem1  47141  ovnsubadd  47143  hsphoif  47147  hoidmvval  47148  hsphoival  47150  hoidmvlelem3  47168  hoidmvlelem5  47170  hoidmvle  47171  ovnhoilem1  47172  ovnhoi  47174  ovnlecvr2  47181  ovncvr2  47182  hoidifhspval2  47186  hoiqssbllem2  47194  hspmbllem2  47198  hspmbllem3  47199  hspmbl  47200  ovnovollem1  47227  smfmullem2  47363  smfmul  47366  smfpimcclem  47378  chnerlem1  47455  nthrucw  47459  sinnpoly  47482  cfsetsnfsetfv  47648  cfsetsnfsetfo  47651  iccpart  48019  iccpartiun  48037  icceuelpart  48039  nnsum3primes4  48407  nnsum3primesgbe  48411  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  bgoldbtbnd  48428  isisubgr  48481  isgrim  48501  grimidvtxedg  48504  grimcnv  48507  grimco  48508  isuspgrim0  48513  gricushgr  48536  ushggricedg  48546  uhgrimisgrgric  48550  isgrtri  48562  isubgr3stgrlem3  48587  isubgr3stgr  48594  isgrlim  48601  uspgrlim  48611  grlicref  48631  grlicsym  48632  grlictr  48634  grlimedgnedg  48750  isupwlk  48755  lincval  49028  lincdifsn  49043  linindslinci  49067  lindslinindsimp1  49076  linds0  49084  el0ldep  49085  lindsrng01  49087  snlindsntorlem  49089  ldepspr  49092  islindeps2  49102  zlmodzxzldep  49123  bigoval  49168  elbigo  49170  0aryfvalelfv  49254  1arympt1fv  49258  1arymaptfv  49259  1arymaptfo  49262  2arymptfv  49269  2arymaptfv  49270  2arymaptfo  49273  prelrrx2b  49333  rrx2plord  49339  rrx2vlinest  49360  rrx2linesl  49362  elrrx2linest2  49364  line2ylem  49370  line2xlem  49372  itsclc0  49390  itsclc0b  49391  itscnhlinecirc02p  49404  elfvne0  49467  iinfprg  49677  thincciso  50071  thinccisod  50072  setrecseq  50303  aacllem  50419