Theorem fveq1 6881

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 5115	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6521	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6545	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6545	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2829	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113  ℩cio 6491  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545

This theorem is referenced by:  fveq1i  6883  fveq1d  6884  iffv  6899  fvmptd3f  7006  fvmptdv2  7009  eqfnun  7033  fsnex  7282  f1prex  7283  isoeq1  7316  oveq  7417  elovmpt3imp  7668  ofrfvalg  7683  offval  7684  offval3  7978  bropopvvv  8084  bropfvvvvlem  8085  poseq  8153  soseq  8154  frrlem1  8282  frrlem13  8294  smoeq  8336  tfrlem12  8375  tz7.44-2  8393  tz7.44-3  8394  rdgeq1  8397  fsetfocdm  8857  fsetprcnex  8858  mapsncnv  8890  elixp2  8898  resixpfo  8933  elixpsn  8934  mapsnend  9032  enfixsn  9073  mapxpen  9130  ac6sfi  9243  ordtypelem7  9485  wemaplem1  9507  ixpiunwdom  9551  oemapval  9651  cantnf  9661  wemapwe  9665  cnfcom3clem  9673  ssttrcl  9683  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  updjud  9919  infxpenc2lem2  10003  fseqenlem1  10007  dfac8clem  10015  ac5num  10019  acni  10028  acni2  10029  acnlem  10031  dfac4  10105  dfac5lem5  10110  dfac2a  10112  dfac9  10119  dfacacn  10124  dfac12lem1  10126  dfac12r  10129  cofsmo  10252  cfsmolem  10253  cfsmo  10254  cfcoflem  10255  coftr  10256  alephsing  10259  isfin3ds  10312  fin23lem17  10321  fin23lem32  10327  fin23lem39  10333  isf33lem  10349  isf34lem6  10363  axcc2lem  10419  axcc3  10421  axdc2lem  10431  axdc3lem2  10434  axdc3lem3  10435  axdc3  10437  axdc4lem  10438  axcclem  10440  ac6num  10462  axdclem2  10503  konigthlem  10552  inar1  10759  1fv  13674  axdc4uzlem  14018  seqeq3  14041  seqof  14094  ccatfval  14609  wrdl1s1  14651  ccat1st1st  14665  cshf1  14846  cshweqrep  14857  wrdlen2i  14978  wwlktovf  14992  wwlktovf1  14993  wwlktovfo  14994  wrd2f1tovbij  14996  rtrclreclem1  15093  dfrtrclrec2  15094  rtrclreclem2  15095  rtrclreclem4  15097  dfrtrcl2  15098  clim  15544  rlim  15545  ello1  15565  elo1  15576  summo  15767  fsum  15770  prodmo  15989  fprod  15994  bpolylem  16101  bpolyval  16102  vdwlem6  17045  vdwlem8  17047  ramcl  17088  strfvnd  17244  prdsplusgval  17525  prdsmulrval  17527  prdsleval  17529  prdsdsval  17530  prdsvscaval  17531  xpsff1o  17620  isacs2  17708  isnat  18006  yonedalem3b  18334  yonedainv  18336  ischn  18662  chnind  18676  chnub  18677  ismgmhm  18753  ismhm  18842  prdspjmhm  18887  isgrpinv  19059  pwsmulg  19184  isghm  19285  cayleylem2  19482  symgfix2  19485  gsmsymgrfix  19497  gsmsymgreq  19501  symgfixelq  19502  pmtr3ncomlem2  19543  pmtrdifel  19549  pmtrdifwrdel  19554  pmtrdifwrdel2  19555  psgnunilem2  19564  psgnunilem3  19565  efgsdm  19799  efgredlemd  19813  efgredlem  19816  efgred  19817  efgrelexlema  19818  efgrelexlemb  19819  prdsgsum  20050  pwspjmhmmgpd  20408  pwsexpg  20409  pwsgprod  20410  isrnghm  20522  isabv  20891  islmhm  21125  frgpcyg  21691  psgndiflemB  21718  psgndiflemA  21719  dsmmelbas  21857  frlmipval  21897  frlmphl  21899  uvcf1  21910  islindf  21930  islindf4  21956  psrmulfval  22061  evlslem2  22198  evlslem3  22199  evlslem1  22201  mpfrcl  22204  evlsvval  22209  evlsvvval  22212  selvval  22239  mplmapghm  22241  evlsvarval  22246  selvvvval  22261  psdval  22290  psdcoef  22291  psdadd  22294  psdmul  22297  psdmvr  22300  coe1fval  22333  coe1mul2lem2  22397  coe1tm  22402  madetsumid  22586  mvmulval  22668  marepvval0  22691  mulmarep1gsum2  22699  mdetleib2  22713  m1detdiag  22722  mdetralt  22733  mdetunilem7  22743  mdetunilem9  22745  m2detleiblem3  22754  m2detleiblem4  22755  m2detleib  22756  symgmatr01lem  22778  gsummatr01lem1  22780  gsummatr01lem4  22783  gsummatr01  22784  smadiadetlem3  22793  pmatcoe1fsupp  22826  pmatcollpw3lem  22908  pmatcollpw3fi1lem2  22912  iscnp  23362  1stcfb  23570  ptpjpre1  23696  elpt  23697  elptr  23698  ptpjopn  23737  dfac14  23743  upxp  23748  pthaus  23763  ptrescn  23764  xkoptsub  23779  cnmptkp  23805  xkofvcn  23809  cnmptk1p  23810  cnmptk2  23811  ptunhmeo  23933  ptcmplem3  24179  ptcmplem4  24180  symgtgp  24231  prdstmdd  24249  isucn  24402  imasdsf1olem  24498  prdsxmslem2  24654  tngngp3  24781  nmoval  24840  elcncf  25016  ishtpy  25099  pcoval  25138  om1elbas  25159  elpi1i  25173  iscau  25403  rrxds  25520  rrxdsfival  25540  ehl1eudisval  25548  ehl2eudisval  25550  mbfi1fseqlem6  25847  mbfi1flimlem  25849  isibl  25892  deg1ldg  26217  deg1leb  26220  elply2  26321  elplyr  26326  ne0p  26332  coeeu  26350  coelem  26351  coeeq  26352  coeidlem  26362  elqaalem3  26450  qaa  26452  iaa  26454  aareccl  26455  aannenlem2  26458  aaliou2  26469  dchrptlem2  27394  dchrpt  27396  dchrsum2  27397  sumdchr2  27399  dchrvmaeq0  27633  rpvmasum2  27641  dchrisum0re  27642  ostth  27768  ltsval  27776  nolesgn2o  27800  nogesgn1o  27802  noresle  27826  nosupprefixmo  27829  noinfprefixmo  27830  nosupcbv  27831  nosupfv  27835  noinfcbv  27846  noinffv  27850  iscgrg  28746  isismt  28768  israg  28935  iseqlg  29138  brbtwn  29189  brbtwn2  29195  colinearalg  29200  axsegconlem1  29207  axsegcon  29217  ax5seglem5  29223  axpasch  29231  axlowdim  29251  axeuclidlem  29252  axcontlem1  29254  axcontlem2  29255  axcontlem5  29258  vtxdgfval  29757  1egrvtxdg1  29799  isewlk  29892  iswlk  29900  uspgr2wlkeq2  29936  iswlkon  29945  isclwlk  30062  iscrct  30079  iscycl  30080  iswwlks  30125  wwlknon  30146  wlkiswwlks2  30164  wwlksnredwwlkn0  30185  wlksnwwlknvbij  30197  wwlksnextproplem3  30200  wwlksnextprop  30201  umgr2wlk  30238  midwwlks2s3  30241  elwwlks2  30258  elwspths2spth  30259  rusgrnumwwlkslem  30261  rusgrnumwwlkb0  30263  rusgrnumwwlks  30266  isclwwlk  30275  clwlkclwwlklem1  30290  clwwlkn1loopb  30334  clwwlkel  30337  clwwlkf  30338  clwwlkf1  30340  isclwwlknon  30382  clwwlknon1  30388  s2elclwwlknon2  30395  clwwlkvbij  30404  uhgr3cyclex  30473  fusgreg2wsplem  30624  fusgr2wsp2nb  30625  fusgreghash2wsp  30629  2clwwlkel  30640  extwwlkfabel  30644  numclwwlk1lem2fv  30647  numclwwlk1lem2  30651  clwwlknonclwlknonf1o  30653  dlwwlknondlwlknonf1o  30656  numclwwlk2lem1  30667  numclwlk2lem2f  30668  numclwlk2lem2f1o  30670  ex-fv  30734  isnvlem  30902  islno  31045  nmooval  31055  nmblolbi  31092  isphg  31109  ajmoi  31150  ajval  31153  ubthlem3  31164  htthlem  31209  hcau  31476  hlimi  31480  hosmval  32027  hommval  32028  hodmval  32029  hfsmval  32030  hfmmval  32031  adjmo  32124  nmopval  32148  elcnop  32149  ellnop  32150  elunop  32164  elhmop  32165  nmfnval  32168  elcnfn  32174  ellnfn  32175  adjeu  32181  adjval  32182  eigvecval  32188  eigvalfval  32189  adj1  32225  adjeq  32227  hmopadj2  32233  lnopeq0i  32299  lnopeq  32301  elunop2  32305  lnophm  32311  hmopco  32315  nmbdoplb  32317  nmcoplb  32322  lnopcon  32327  lnfn0  32339  lnfnmul  32340  nmbdfnlb  32342  nmcfnlb  32346  lnfncon  32348  riesz4  32356  riesz1  32357  cnlnadjlem9  32367  cnlnadjeu  32370  cnlnssadj  32372  nmopcoi  32387  bra11  32400  cnvbraval  32402  pjss2coi  32456  pjssdif2i  32466  pjssdif1i  32467  pjclem4  32491  pj3si  32499  pj3cor1i  32501  isst  32505  ishst  32506  stri  32549  hstri  32557  aciunf1lem  32947  ismnt  33243  mgcval  33247  fzo0pmtrlast  33352  elrgspnlem1  33502  elrgspnlem2  33503  elrgspnlem3  33504  elrgspnlem4  33505  elrgspn  33506  elrgspnsubrunlem1  33507  linds2eq  33637  elrspunidl  33679  elrspunsn  33680  dfufd2lem  33783  psrnzr  33846  0mplrim  33848  0mplric  33849  selvply1rhmlema  33852  selvply1rhmlemb  33853  selvply1rhmlem1  33854  selvply1rhmlem3  33856  selvply1rhmlem5  33858  selvply1rhm  33859  mplidom  33862  extvfv  33867  extvfvv  33868  extvfvcl  33870  evlvarval  33875  evlextv  33876  mplvrpmga  33879  splysubrg  33894  issply  33895  vietalem  33913  vieta  33914  lbsdiflsp0  33960  fedgmullem1  33963  fedgmullem2  33964  fedgmul  33965  fldextrspunlsplem  34007  fldextrspunlsp  34008  fldext2chn  34062  constrextdg2lem  34082  constrextdg2  34083  lmatval  34147  mdetpmtr1  34157  zarcmplem  34215  ismeas  34533  isrnmeas  34534  cntnevol  34562  carsgval  34637  sitgval  34666  eulerpartleme  34697  eulerpartlemd  34700  eulerpartlemr  34708  eulerpartlemgvv  34710  eulerpart  34716  cndprobval  34767  signstfvneq0  34903  reprsum  34944  reprsuc  34946  reprpmtf1o  34957  reprdifc  34958  breprexp  34964  vtsval  34968  hgt750lemb  34987  hgt750lema  34988  hgt750leme  34989  bnj66  35192  bnj106  35200  bnj125  35204  bnj154  35210  bnj155  35211  bnj526  35220  bnj540  35224  bnj609  35249  bnj611  35250  bnj893  35260  bnj1000  35273  bnj1014  35293  bnj1015  35294  bnj1234  35345  bnj1463  35387  fineqvnttrclse  35459  gblacfnacd  35484  loop1cycl  35527  derangenlem  35561  subfacp1lem3  35572  subfacp1lem5  35574  subfacp1lem6  35575  subfacp1  35576  sconnpht  35619  cnpconn  35620  txpconn  35622  ptpconn  35623  indispconn  35624  connpconn  35625  cvxpconn  35632  cvmliftmo  35674  cvmliftlem14  35687  cvmliftlem15  35688  cvmliftiota  35691  cvmlift2  35706  cvmliftphtlem  35707  cvmlift3lem2  35710  cvmlift3lem6  35714  cvmlift3lem7  35715  cvmlift3lem9  35717  cvmlift3  35718  satfv1lem  35752  satfv1  35753  sategoelfvb  35809  mrsubff1  35904  mrsub0  35906  mrsubccat  35908  mrsubcn  35909  elmsubrn  35918  msubrn  35919  msubco  35921  msubvrs  35950  mclsax  35959  shftvalg  36122  fwddifval  36552  fwddifnval  36553  bj-evalval  37604  unceq  38135  matunitlindflem2  38155  poimirlem17  38175  poimirlem20  38178  poimirlem22  38180  poimirlem23  38181  poimirlem27  38185  poimirlem28  38186  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  poimir  38191  broucube  38192  voliunnfl  38202  volsupnfl  38203  itg2addnclem  38209  itg2addnclem3  38211  itg2addnc  38212  ftc1anclem2  38232  ftc1anclem5  38235  upixp  38267  fdc  38283  isismty  38339  rrnmval  38366  elghomlem2OLD  38424  isrngohom  38503  islfl  39723  isopos  39843  islaut  40746  ispautN  40762  isldil  40773  isltrn  40782  ltrnid  40798  ltrneq2  40811  isdilN  40817  istrnN  40820  trlval  40825  ltrneq3  40871  cdleme50ex  41222  cdleme  41223  cdlemg1a  41233  ltrniotaval  41244  ltrniotavalbN  41247  cdlemeiota  41248  cdlemg2jlemOLDN  41256  cdlemg2fvlem  41257  cdlemg2klem  41258  istendo  41423  tendoplcbv  41438  tendopl  41439  tendoicbv  41456  tendoi  41457  tendoid0  41488  tendo1ne0  41491  cdlemksv2  41510  cdlemkuv2  41530  cdlemk33N  41572  cdlemk34  41573  cdlemk36  41576  cdlemk19u  41633  cdlemk  41637  tendoex  41638  dvavsca  41680  dvhvscacbv  41761  dvhvscaval  41762  dicopelval  41840  dicelval1sta  41850  diclspsn  41857  dihmeetlem13N  41982  dih1dimatlem0  41991  dih1dimatlem  41992  dihpN  41999  islpolN  42146  hdmap1fval  42459  hdmapfval  42490  sticksstones1  42802  sticksstones2  42803  sticksstones3  42804  sticksstones8  42809  sticksstones10  42811  sticksstones11  42812  sticksstones12a  42813  sticksstones12  42814  sticksstones15  42817  frlmsnic  43199  uvcn0  43201  evlsbagval  43209  evlselv  43212  fsuppssindlem2  43215  fsuppssind  43216  prjspnfv01  43247  prjspner01  43248  prjspner1  43249  sn-isghm  43296  ismrc  43323  mzpclval  43347  mzpsubst  43370  mzprename  43371  mzpcompact2lem  43373  eldioph  43380  eldioph2  43384  eldioph2b  43385  eldioph3  43388  rexrabdioph  43412  2rexfrabdioph  43414  3rexfrabdioph  43415  4rexfrabdioph  43416  6rexfrabdioph  43417  7rexfrabdioph  43418  eldioph4i  43430  rabren3dioph  43433  mzpcong  43590  jm2.27dlem1  43627  wepwsolem  43660  aomclem6  43677  aomclem8  43679  dfac11  43680  dgraalem  43763  dgraaub  43766  dgraa0p  43767  mpaaeu  43768  mpaalem  43770  aaitgo  43780  rngunsnply  43787  cantnfresb  43942  tfsconcatun  43955  nvocnvb  44039  eliunov2  44296  rfovcnvfvd  44624  fsovfvd  44627  fsovcnvlem  44630  dssmapfv2d  44635  dssmapnvod  44637  clsk1independent  44663  ntrclskb  44686  ntrclsk13  44688  gneispace2  44749  mnringmulrvald  44842  dvconstbi  44935  addrval  45065  subrval  45066  mulvval  45067  relpeq1  45544  fnchoice  45640  refsum2cnlem1  45648  choicefi  45808  axccdom  45829  fmulcl  46188  fmuldfeqlem1  46189  mccllem  46204  mccl  46205  climf  46229  climf2  46271  dvnprodlem1  46551  dvnprodlem3  46553  dvnprod  46554  stoweidlem2  46607  stoweidlem6  46611  stoweidlem8  46613  stoweidlem9  46614  stoweidlem15  46620  stoweidlem16  46621  stoweidlem17  46622  stoweidlem18  46623  stoweidlem21  46626  stoweidlem27  46632  stoweidlem31  46636  stoweidlem36  46641  stoweidlem37  46642  stoweidlem41  46646  stoweidlem43  46648  stoweidlem44  46649  stoweidlem45  46650  stoweidlem46  46651  stoweidlem48  46653  stoweidlem51  46656  stoweidlem55  46660  stoweidlem59  46664  stoweidlem60  46665  stoweidlem62  46667  fourierdlem2  46714  fourierdlem3  46715  elaa2lem  46838  etransclem11  46850  etransclem24  46863  etransclem26  46865  etransclem28  46867  etransclem35  46874  rrndistlt  46895  ioorrnopn  46910  subsaliuncllem  46962  sge0val  46971  ismea  47056  caragenval  47098  isome  47099  isomenndlem  47135  hoicvrrex  47161  ovnlecvr  47163  ovncvrrp  47169  ovn0lem  47170  ovnsubaddlem1  47175  ovnsubadd  47177  hsphoif  47181  hoidmvval  47182  hsphoival  47184  hoidmvlelem3  47202  hoidmvlelem5  47204  hoidmvle  47205  ovnhoilem1  47206  ovnhoi  47208  ovnlecvr2  47215  ovncvr2  47216  hoidifhspval2  47220  hoiqssbllem2  47228  hspmbllem2  47232  hspmbllem3  47233  hspmbl  47234  ovnovollem1  47261  smfmullem2  47397  smfmul  47400  smfpimcclem  47412  chnerlem1  47489  nthrucw  47493  sinnpoly  47516  cfsetsnfsetfv  47682  cfsetsnfsetfo  47685  iccpart  48053  iccpartiun  48071  icceuelpart  48073  nnsum3primes4  48441  nnsum3primesgbe  48445  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  bgoldbtbnd  48462  isisubgr  48515  isgrim  48535  grimidvtxedg  48538  grimcnv  48541  grimco  48542  isuspgrim0  48547  gricushgr  48570  ushggricedg  48580  uhgrimisgrgric  48584  isgrtri  48596  isubgr3stgrlem3  48621  isubgr3stgr  48628  isgrlim  48635  uspgrlim  48645  grlicref  48665  grlicsym  48666  grlictr  48668  grlimedgnedg  48784  isupwlk  48789  lincval  49073  lincdifsn  49088  linindslinci  49112  lindslinindsimp1  49121  linds0  49129  el0ldep  49130  lindsrng01  49132  snlindsntorlem  49134  ldepspr  49137  islindeps2  49147  zlmodzxzldep  49168  bigoval  49213  elbigo  49215  0aryfvalelfv  49299  1arympt1fv  49303  1arymaptfv  49304  1arymaptfo  49307  2arymptfv  49314  2arymaptfv  49315  2arymaptfo  49318  prelrrx2b  49378  rrx2plord  49384  rrx2vlinest  49405  rrx2linesl  49407  elrrx2linest2  49409  line2ylem  49415  line2xlem  49417  itsclc0  49435  itsclc0b  49436  itscnhlinecirc02p  49449  elfvne0  49511  iinfprg  49721  thincciso  50115  thinccisod  50116  setrecseq  50347  aacllem  50474