Theorem fveq1 6891

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 5151	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6528	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6552	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6552	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5149  ℩cio 6494  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552

This theorem is referenced by:  fveq1i  6893  fveq1d  6894  iffv  6909  fvmptd3f  7014  fvmptdv2  7017  eqfnun  7039  fsnex  7281  f1prex  7282  isoeq1  7314  oveq  7415  elovmpt3imp  7663  ofrfvalg  7678  offval  7679  offval3  7969  bropopvvv  8076  bropfvvvvlem  8077  poseq  8144  soseq  8145  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  smoeq  8350  tfrlem12  8389  tz7.44-2  8407  tz7.44-3  8408  rdgeq1  8411  fsetfocdm  8855  fsetprcnex  8856  mapsncnv  8887  elixp2  8895  resixpfo  8930  elixpsn  8931  mapsnend  9036  enfixsn  9081  mapxpen  9143  ac6sfi  9287  ordtypelem7  9519  wemaplem1  9541  ixpiunwdom  9585  oemapval  9678  cantnf  9688  wemapwe  9692  cnfcom3clem  9700  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  updjud  9929  infxpenc2lem2  10015  fseqenlem1  10019  dfac8clem  10027  ac5num  10031  acni  10040  acni2  10041  acnlem  10043  dfac4  10117  dfac5lem5  10122  dfac2a  10124  dfac9  10131  dfacacn  10136  dfac12lem1  10138  dfac12r  10141  cofsmo  10264  cfsmolem  10265  cfsmo  10266  cfcoflem  10267  coftr  10268  alephsing  10271  isfin3ds  10324  fin23lem17  10333  fin23lem32  10339  fin23lem39  10345  isf33lem  10361  isf34lem6  10375  axcc2lem  10431  axcc3  10433  axdc2lem  10443  axdc3lem2  10446  axdc3lem3  10447  axdc3  10449  axdc4lem  10450  axcclem  10452  ac6num  10474  axdclem2  10515  konigthlem  10563  inar1  10770  1fv  13620  axdc4uzlem  13948  seqeq3  13971  seqof  14025  ccatfval  14523  wrdl1s1  14564  ccat1st1st  14578  cshf1  14760  cshweqrep  14771  wrdlen2i  14893  wwlktovf  14907  wwlktovf1  14908  wwlktovfo  14909  wrd2f1tovbij  14911  rtrclreclem1  15004  dfrtrclrec2  15005  rtrclreclem2  15006  rtrclreclem4  15008  dfrtrcl2  15009  clim  15438  rlim  15439  ello1  15459  elo1  15470  summo  15663  fsum  15666  prodmo  15880  fprod  15885  bpolylem  15992  bpolyval  15993  vdwlem6  16919  vdwlem8  16921  ramcl  16962  strfvnd  17118  prdsplusgval  17419  prdsmulrval  17421  prdsleval  17423  prdsdsval  17424  prdsvscaval  17425  xpsff1o  17513  isacs2  17597  isnat  17898  yonedalem3b  18232  yonedainv  18234  ismhm  18673  prdspjmhm  18710  isgrpinv  18878  pwsmulg  18999  isghm  19092  cayleylem2  19281  symgfix2  19284  gsmsymgrfix  19296  gsmsymgreq  19300  symgfixelq  19301  pmtr3ncomlem2  19342  pmtrdifel  19348  pmtrdifwrdel  19353  pmtrdifwrdel2  19354  psgnunilem2  19363  psgnunilem3  19364  efgsdm  19598  efgredlemd  19612  efgredlem  19615  efgred  19616  efgrelexlema  19617  efgrelexlemb  19618  prdsgsum  19849  pwspjmhmmgpd  20141  pwsexpg  20142  isabv  20427  islmhm  20638  frgpcyg  21129  psgndiflemB  21153  psgndiflemA  21154  dsmmelbas  21294  frlmipval  21334  frlmphl  21336  uvcf1  21347  islindf  21367  islindf4  21393  psrmulfval  21504  evlslem2  21642  evlslem3  21643  evlslem1  21645  mpfrcl  21648  selvval  21681  coe1fval  21729  coe1mul2lem2  21790  coe1tm  21795  madetsumid  21963  mvmulval  22045  marepvval0  22068  mulmarep1gsum2  22076  mdetleib2  22090  m1detdiag  22099  mdetralt  22110  mdetunilem7  22120  mdetunilem9  22122  m2detleiblem3  22131  m2detleiblem4  22132  m2detleib  22133  symgmatr01lem  22155  gsummatr01lem1  22157  gsummatr01lem4  22160  gsummatr01  22161  smadiadetlem3  22170  pmatcoe1fsupp  22203  pmatcollpw3lem  22285  pmatcollpw3fi1lem2  22289  iscnp  22741  1stcfb  22949  ptpjpre1  23075  elpt  23076  elptr  23077  ptpjopn  23116  dfac14  23122  upxp  23127  pthaus  23142  ptrescn  23143  xkoptsub  23158  cnmptkp  23184  xkofvcn  23188  cnmptk1p  23189  cnmptk2  23190  ptunhmeo  23312  ptcmplem3  23558  ptcmplem4  23559  symgtgp  23610  prdstmdd  23628  isucn  23783  imasdsf1olem  23879  prdsxmslem2  24038  tngngp3  24173  nmoval  24232  elcncf  24405  ishtpy  24488  pcoval  24527  om1elbas  24548  elpi1i  24562  iscau  24793  rrxds  24910  rrxdsfival  24930  ehl1eudisval  24938  ehl2eudisval  24940  mbfi1fseqlem6  25238  mbfi1flimlem  25240  isibl  25283  deg1ldg  25610  deg1leb  25613  elply2  25710  elplyr  25715  ne0p  25721  coeeu  25739  coelem  25740  coeeq  25741  coeidlem  25751  elqaalem3  25834  qaa  25836  iaa  25838  aareccl  25839  aannenlem2  25842  aaliou2  25853  dchrptlem2  26768  dchrpt  26770  dchrsum2  26771  sumdchr2  26773  dchrvmaeq0  27007  rpvmasum2  27015  dchrisum0re  27016  ostth  27142  sltval  27150  nolesgn2o  27174  nogesgn1o  27176  noresle  27200  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupfv  27209  noinfcbv  27220  noinffv  27224  iscgrg  27763  isismt  27785  israg  27948  iseqlg  28118  brbtwn  28157  brbtwn2  28163  colinearalg  28168  axsegconlem1  28175  axsegcon  28185  ax5seglem5  28191  axpasch  28199  axlowdim  28219  axeuclidlem  28220  axcontlem1  28222  axcontlem2  28223  axcontlem5  28226  vtxdgfval  28724  1egrvtxdg1  28766  isewlk  28859  iswlk  28867  uspgr2wlkeq2  28904  iswlkon  28914  isclwlk  29030  iscrct  29047  iscycl  29048  iswwlks  29090  wwlknon  29111  wlkiswwlks2  29129  wwlksnredwwlkn0  29150  wlksnwwlknvbij  29162  wwlksnextproplem3  29165  wwlksnextprop  29166  umgr2wlk  29203  midwwlks2s3  29206  elwwlks2  29220  elwspths2spth  29221  rusgrnumwwlkslem  29223  rusgrnumwwlkb0  29225  rusgrnumwwlks  29228  isclwwlk  29237  clwlkclwwlklem1  29252  clwwlkn1loopb  29296  clwwlkel  29299  clwwlkf  29300  clwwlkf1  29302  isclwwlknon  29344  clwwlknon1  29350  s2elclwwlknon2  29357  clwwlkvbij  29366  uhgr3cyclex  29435  fusgreg2wsplem  29586  fusgr2wsp2nb  29587  fusgreghash2wsp  29591  2clwwlkel  29602  extwwlkfabel  29606  numclwwlk1lem2fv  29609  numclwwlk1lem2  29613  clwwlknonclwlknonf1o  29615  dlwwlknondlwlknonf1o  29618  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  ex-fv  29696  isnvlem  29863  islno  30006  nmooval  30016  nmblolbi  30053  isphg  30070  ajmoi  30111  ajval  30114  ubthlem3  30125  htthlem  30170  hcau  30437  hlimi  30441  hosmval  30988  hommval  30989  hodmval  30990  hfsmval  30991  hfmmval  30992  adjmo  31085  nmopval  31109  elcnop  31110  ellnop  31111  elunop  31125  elhmop  31126  nmfnval  31129  elcnfn  31135  ellnfn  31136  adjeu  31142  adjval  31143  eigvecval  31149  eigvalfval  31150  adj1  31186  adjeq  31188  hmopadj2  31194  lnopeq0i  31260  lnopeq  31262  elunop2  31266  lnophm  31272  hmopco  31276  nmbdoplb  31278  nmcoplb  31283  lnopcon  31288  lnfn0  31300  lnfnmul  31301  nmbdfnlb  31303  nmcfnlb  31307  lnfncon  31309  riesz4  31317  riesz1  31318  cnlnadjlem9  31328  cnlnadjeu  31331  cnlnssadj  31333  nmopcoi  31348  bra11  31361  cnvbraval  31363  pjss2coi  31417  pjssdif2i  31427  pjssdif1i  31428  pjclem4  31452  pj3si  31460  pj3cor1i  31462  isst  31466  ishst  31467  stri  31510  hstri  31518  aciunf1lem  31887  ismnt  32153  mgcval  32157  linds2eq  32497  elrspunidl  32546  elrspunsn  32547  lbsdiflsp0  32711  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  lmatval  32793  mdetpmtr1  32803  zarcmplem  32861  ismeas  33197  isrnmeas  33198  cntnevol  33226  carsgval  33302  sitgval  33331  eulerpartleme  33362  eulerpartlemd  33365  eulerpartlemr  33373  eulerpartlemgvv  33375  eulerpart  33381  cndprobval  33432  signstfvneq0  33583  reprsum  33625  reprsuc  33627  reprpmtf1o  33638  reprdifc  33639  breprexp  33645  vtsval  33649  hgt750lemb  33668  hgt750lema  33669  hgt750leme  33670  bnj66  33871  bnj106  33879  bnj125  33883  bnj154  33889  bnj155  33890  bnj526  33899  bnj540  33903  bnj609  33928  bnj611  33929  bnj893  33939  bnj1000  33952  bnj1014  33972  bnj1015  33973  bnj1234  34024  bnj1463  34066  loop1cycl  34128  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  subfacp1  34177  sconnpht  34220  cnpconn  34221  txpconn  34223  ptpconn  34224  indispconn  34225  connpconn  34226  cvxpconn  34233  cvmliftmo  34275  cvmliftlem14  34288  cvmliftlem15  34289  cvmliftiota  34292  cvmlift2  34307  cvmliftphtlem  34308  cvmlift3lem2  34311  cvmlift3lem6  34315  cvmlift3lem7  34316  cvmlift3lem9  34318  cvmlift3  34319  satfv1lem  34353  satfv1  34354  sategoelfvb  34410  mrsubff1  34505  mrsub0  34507  mrsubccat  34509  mrsubcn  34510  elmsubrn  34519  msubrn  34520  msubco  34522  msubvrs  34551  mclsax  34560  shftvalg  34701  fwddifval  35134  fwddifnval  35135  bj-evalval  35956  unceq  36465  matunitlindflem2  36485  poimirlem17  36505  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem27  36515  poimirlem28  36516  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  poimir  36521  broucube  36522  voliunnfl  36532  volsupnfl  36533  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  ftc1anclem2  36562  ftc1anclem5  36565  upixp  36597  fdc  36613  isismty  36669  rrnmval  36696  elghomlem2OLD  36754  isrngohom  36833  islfl  37930  isopos  38050  islaut  38954  ispautN  38970  isldil  38981  isltrn  38990  ltrnid  39006  ltrneq2  39019  isdilN  39025  istrnN  39028  trlval  39033  ltrneq3  39079  cdleme50ex  39430  cdleme  39431  cdlemg1a  39441  ltrniotaval  39452  ltrniotavalbN  39455  cdlemeiota  39456  cdlemg2jlemOLDN  39464  cdlemg2fvlem  39465  cdlemg2klem  39466  istendo  39631  tendoplcbv  39646  tendopl  39647  tendoicbv  39664  tendoi  39665  tendoid0  39696  tendo1ne0  39699  cdlemksv2  39718  cdlemkuv2  39738  cdlemk33N  39780  cdlemk34  39781  cdlemk36  39784  cdlemk19u  39841  cdlemk  39845  tendoex  39846  dvavsca  39888  dvhvscacbv  39969  dvhvscaval  39970  dicopelval  40048  dicelval1sta  40058  diclspsn  40065  dihmeetlem13N  40190  dih1dimatlem0  40199  dih1dimatlem  40200  dihpN  40207  islpolN  40354  hdmap1fval  40667  hdmapfval  40698  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones8  40969  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones15  40977  frlmsnic  41110  uvcn0  41112  pwsgprod  41114  mplmapghm  41128  evlsvval  41132  evlsvvval  41135  evlsvarval  41137  evlsbagval  41138  selvvvval  41157  evlselv  41159  fsuppssindlem2  41164  fsuppssind  41165  prjspnfv01  41366  prjspner01  41367  prjspner1  41368  ismrc  41439  mzpclval  41463  mzpsubst  41486  mzprename  41487  mzpcompact2lem  41489  eldioph  41496  eldioph2  41500  eldioph2b  41501  eldioph3  41504  rexrabdioph  41532  2rexfrabdioph  41534  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  eldioph4i  41550  rabren3dioph  41553  mzpcong  41711  jm2.27dlem1  41748  wepwsolem  41784  aomclem6  41801  aomclem8  41803  dfac11  41804  dgraalem  41887  dgraaub  41890  dgraa0p  41891  mpaaeu  41892  mpaalem  41894  aaitgo  41904  rngunsnply  41915  cantnfresb  42074  tfsconcatun  42087  nvocnvb  42173  eliunov2  42430  rfovcnvfvd  42758  fsovfvd  42761  fsovcnvlem  42764  dssmapfv2d  42769  dssmapnvod  42771  clsk1independent  42797  ntrclskb  42820  ntrclsk13  42822  gneispace2  42883  mnringmulrvald  42986  dvconstbi  43093  addrval  43225  subrval  43226  mulvval  43227  fnchoice  43713  refsum2cnlem1  43721  choicefi  43899  axccdom  43921  fmulcl  44297  fmuldfeqlem1  44298  mccllem  44313  mccl  44314  climf  44338  climf2  44382  dvnprodlem1  44662  dvnprodlem3  44664  dvnprod  44665  stoweidlem2  44718  stoweidlem6  44722  stoweidlem8  44724  stoweidlem9  44725  stoweidlem15  44731  stoweidlem16  44732  stoweidlem17  44733  stoweidlem18  44734  stoweidlem21  44737  stoweidlem27  44743  stoweidlem31  44747  stoweidlem36  44752  stoweidlem37  44753  stoweidlem41  44757  stoweidlem43  44759  stoweidlem44  44760  stoweidlem45  44761  stoweidlem46  44762  stoweidlem48  44764  stoweidlem51  44767  stoweidlem55  44771  stoweidlem59  44775  stoweidlem60  44776  stoweidlem62  44778  fourierdlem2  44825  fourierdlem3  44826  elaa2lem  44949  etransclem11  44961  etransclem24  44974  etransclem26  44976  etransclem28  44978  etransclem35  44985  rrndistlt  45006  ioorrnopn  45021  subsaliuncllem  45073  sge0val  45082  ismea  45167  caragenval  45209  isome  45210  isomenndlem  45246  hoicvrrex  45272  ovnlecvr  45274  ovncvrrp  45280  ovn0lem  45281  ovnsubaddlem1  45286  ovnsubadd  45288  hsphoif  45292  hoidmvval  45293  hsphoival  45295  hoidmvlelem3  45313  hoidmvlelem5  45315  hoidmvle  45316  ovnhoilem1  45317  ovnhoi  45319  ovnlecvr2  45326  ovncvr2  45327  hoidifhspval2  45331  hoiqssbllem2  45339  hspmbllem2  45343  hspmbllem3  45344  hspmbl  45345  ovnovollem1  45372  smfmullem2  45508  smfmul  45511  smfpimcclem  45523  tworepnotupword  45600  cfsetsnfsetfv  45767  cfsetsnfsetfo  45770  iccpart  46084  iccpartiun  46102  icceuelpart  46104  nnsum3primes4  46456  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbnd  46477  isomgreqve  46493  isomushgr  46494  isomuspgrlem2  46501  isomgrsym  46504  isomgrtr  46507  ushrisomgr  46509  isupwlk  46514  ismgmhm  46553  isrnghm  46690  lincval  47090  lincdifsn  47105  linindslinci  47129  lindslinindsimp1  47138  linds0  47146  el0ldep  47147  lindsrng01  47149  snlindsntorlem  47151  ldepspr  47154  islindeps2  47164  zlmodzxzldep  47185  bigoval  47235  elbigo  47237  0aryfvalelfv  47321  1arympt1fv  47325  1arymaptfv  47326  1arymaptfo  47329  2arymptfv  47336  2arymaptfv  47337  2arymaptfo  47340  prelrrx2b  47400  rrx2plord  47406  rrx2vlinest  47427  rrx2linesl  47429  elrrx2linest2  47431  line2ylem  47437  line2xlem  47439  itsclc0  47457  itsclc0b  47458  itscnhlinecirc02p  47471  elfvne0  47515  thincciso  47669  setrecseq  47730  aacllem  47848