Theorem fveq1 6860

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 5112	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6498	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6522	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6522	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5110  ℩cio 6465  ‘cfv 6514

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522

This theorem is referenced by:  fveq1i  6862  fveq1d  6863  iffv  6878  fvmptd3f  6986  fvmptdv2  6989  eqfnun  7012  fsnex  7261  f1prex  7262  isoeq1  7295  oveq  7396  elovmpt3imp  7649  ofrfvalg  7664  offval  7665  offval3  7964  bropopvvv  8072  bropfvvvvlem  8073  poseq  8140  soseq  8141  frrlem1  8268  frrlem13  8280  smoeq  8322  tfrlem12  8360  tz7.44-2  8378  tz7.44-3  8379  rdgeq1  8382  fsetfocdm  8837  fsetprcnex  8838  mapsncnv  8869  elixp2  8877  resixpfo  8912  elixpsn  8913  mapsnend  9010  enfixsn  9055  mapxpen  9113  ac6sfi  9238  ordtypelem7  9484  wemaplem1  9506  ixpiunwdom  9550  oemapval  9643  cantnf  9653  wemapwe  9657  cnfcom3clem  9665  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  updjud  9894  infxpenc2lem2  9980  fseqenlem1  9984  dfac8clem  9992  ac5num  9996  acni  10005  acni2  10006  acnlem  10008  dfac4  10082  dfac5lem5  10087  dfac2a  10090  dfac9  10097  dfacacn  10102  dfac12lem1  10104  dfac12r  10107  cofsmo  10229  cfsmolem  10230  cfsmo  10231  cfcoflem  10232  coftr  10233  alephsing  10236  isfin3ds  10289  fin23lem17  10298  fin23lem32  10304  fin23lem39  10310  isf33lem  10326  isf34lem6  10340  axcc2lem  10396  axcc3  10398  axdc2lem  10408  axdc3lem2  10411  axdc3lem3  10412  axdc3  10414  axdc4lem  10415  axcclem  10417  ac6num  10439  axdclem2  10480  konigthlem  10528  inar1  10735  1fv  13615  axdc4uzlem  13955  seqeq3  13978  seqof  14031  ccatfval  14545  wrdl1s1  14586  ccat1st1st  14600  cshf1  14782  cshweqrep  14793  wrdlen2i  14915  wwlktovf  14929  wwlktovf1  14930  wwlktovfo  14931  wrd2f1tovbij  14933  rtrclreclem1  15030  dfrtrclrec2  15031  rtrclreclem2  15032  rtrclreclem4  15034  dfrtrcl2  15035  clim  15467  rlim  15468  ello1  15488  elo1  15499  summo  15690  fsum  15693  prodmo  15909  fprod  15914  bpolylem  16021  bpolyval  16022  vdwlem6  16964  vdwlem8  16966  ramcl  17007  strfvnd  17162  prdsplusgval  17443  prdsmulrval  17445  prdsleval  17447  prdsdsval  17448  prdsvscaval  17449  xpsff1o  17537  isacs2  17621  isnat  17919  yonedalem3b  18247  yonedainv  18249  ismgmhm  18630  ismhm  18719  prdspjmhm  18763  isgrpinv  18932  pwsmulg  19058  isghm  19154  isghmOLD  19155  cayleylem2  19350  symgfix2  19353  gsmsymgrfix  19365  gsmsymgreq  19369  symgfixelq  19370  pmtr3ncomlem2  19411  pmtrdifel  19417  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  psgnunilem2  19432  psgnunilem3  19433  efgsdm  19667  efgredlemd  19681  efgredlem  19684  efgred  19685  efgrelexlema  19686  efgrelexlemb  19687  prdsgsum  19918  pwspjmhmmgpd  20244  pwsexpg  20245  isrnghm  20357  isabv  20727  islmhm  20941  frgpcyg  21490  psgndiflemB  21516  psgndiflemA  21517  dsmmelbas  21655  frlmipval  21695  frlmphl  21697  uvcf1  21708  islindf  21728  islindf4  21754  psrmulfval  21859  evlslem2  21993  evlslem3  21994  evlslem1  21996  mpfrcl  21999  selvval  22029  psdval  22053  psdcoef  22054  psdadd  22057  psdmul  22060  psdmvr  22063  coe1fval  22097  coe1mul2lem2  22161  coe1tm  22166  madetsumid  22355  mvmulval  22437  marepvval0  22460  mulmarep1gsum2  22468  mdetleib2  22482  m1detdiag  22491  mdetralt  22502  mdetunilem7  22512  mdetunilem9  22514  m2detleiblem3  22523  m2detleiblem4  22524  m2detleib  22525  symgmatr01lem  22547  gsummatr01lem1  22549  gsummatr01lem4  22552  gsummatr01  22553  smadiadetlem3  22562  pmatcoe1fsupp  22595  pmatcollpw3lem  22677  pmatcollpw3fi1lem2  22681  iscnp  23131  1stcfb  23339  ptpjpre1  23465  elpt  23466  elptr  23467  ptpjopn  23506  dfac14  23512  upxp  23517  pthaus  23532  ptrescn  23533  xkoptsub  23548  cnmptkp  23574  xkofvcn  23578  cnmptk1p  23579  cnmptk2  23580  ptunhmeo  23702  ptcmplem3  23948  ptcmplem4  23949  symgtgp  24000  prdstmdd  24018  isucn  24172  imasdsf1olem  24268  prdsxmslem2  24424  tngngp3  24551  nmoval  24610  elcncf  24789  ishtpy  24878  pcoval  24918  om1elbas  24939  elpi1i  24953  iscau  25183  rrxds  25300  rrxdsfival  25320  ehl1eudisval  25328  ehl2eudisval  25330  mbfi1fseqlem6  25628  mbfi1flimlem  25630  isibl  25673  deg1ldg  26004  deg1leb  26007  elply2  26108  elplyr  26113  ne0p  26119  coeeu  26137  coelem  26138  coeeq  26139  coeidlem  26149  elqaalem3  26236  qaa  26238  iaa  26240  aareccl  26241  aannenlem2  26244  aaliou2  26255  dchrptlem2  27183  dchrpt  27185  dchrsum2  27186  sumdchr2  27188  dchrvmaeq0  27422  rpvmasum2  27430  dchrisum0re  27431  ostth  27557  sltval  27566  nolesgn2o  27590  nogesgn1o  27592  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupfv  27625  noinfcbv  27636  noinffv  27640  iscgrg  28446  isismt  28468  israg  28631  iseqlg  28801  brbtwn  28833  brbtwn2  28839  colinearalg  28844  axsegconlem1  28851  axsegcon  28861  ax5seglem5  28867  axpasch  28875  axlowdim  28895  axeuclidlem  28896  axcontlem1  28898  axcontlem2  28899  axcontlem5  28902  vtxdgfval  29402  1egrvtxdg1  29444  isewlk  29537  iswlk  29545  uspgr2wlkeq2  29582  iswlkon  29592  isclwlk  29710  iscrct  29727  iscycl  29728  iswwlks  29773  wwlknon  29794  wlkiswwlks2  29812  wwlksnredwwlkn0  29833  wlksnwwlknvbij  29845  wwlksnextproplem3  29848  wwlksnextprop  29849  umgr2wlk  29886  midwwlks2s3  29889  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlkslem  29906  rusgrnumwwlkb0  29908  rusgrnumwwlks  29911  isclwwlk  29920  clwlkclwwlklem1  29935  clwwlkn1loopb  29979  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  isclwwlknon  30027  clwwlknon1  30033  s2elclwwlknon2  30040  clwwlkvbij  30049  uhgr3cyclex  30118  fusgreg2wsplem  30269  fusgr2wsp2nb  30270  fusgreghash2wsp  30274  2clwwlkel  30285  extwwlkfabel  30289  numclwwlk1lem2fv  30292  numclwwlk1lem2  30296  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  ex-fv  30379  isnvlem  30546  islno  30689  nmooval  30699  nmblolbi  30736  isphg  30753  ajmoi  30794  ajval  30797  ubthlem3  30808  htthlem  30853  hcau  31120  hlimi  31124  hosmval  31671  hommval  31672  hodmval  31673  hfsmval  31674  hfmmval  31675  adjmo  31768  nmopval  31792  elcnop  31793  ellnop  31794  elunop  31808  elhmop  31809  nmfnval  31812  elcnfn  31818  ellnfn  31819  adjeu  31825  adjval  31826  eigvecval  31832  eigvalfval  31833  adj1  31869  adjeq  31871  hmopadj2  31877  lnopeq0i  31943  lnopeq  31945  elunop2  31949  lnophm  31955  hmopco  31959  nmbdoplb  31961  nmcoplb  31966  lnopcon  31971  lnfn0  31983  lnfnmul  31984  nmbdfnlb  31986  nmcfnlb  31990  lnfncon  31992  riesz4  32000  riesz1  32001  cnlnadjlem9  32011  cnlnadjeu  32014  cnlnssadj  32016  nmopcoi  32031  bra11  32044  cnvbraval  32046  pjss2coi  32100  pjssdif2i  32110  pjssdif1i  32111  pjclem4  32135  pj3si  32143  pj3cor1i  32145  isst  32149  ishst  32150  stri  32193  hstri  32201  aciunf1lem  32593  ismnt  32916  mgcval  32920  ischn  32939  chnind  32944  chnub  32945  fzo0pmtrlast  33056  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  elrgspnsubrunlem1  33205  linds2eq  33359  elrspunidl  33406  elrspunsn  33407  dfufd2lem  33527  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  fldextrspunlsplem  33675  fldextrspunlsp  33676  fldext2chn  33725  constrextdg2lem  33745  constrextdg2  33746  lmatval  33810  mdetpmtr1  33820  zarcmplem  33878  ismeas  34196  isrnmeas  34197  cntnevol  34225  carsgval  34301  sitgval  34330  eulerpartleme  34361  eulerpartlemd  34364  eulerpartlemr  34372  eulerpartlemgvv  34374  eulerpart  34380  cndprobval  34431  signstfvneq0  34570  reprsum  34611  reprsuc  34613  reprpmtf1o  34624  reprdifc  34625  breprexp  34631  vtsval  34635  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  bnj66  34857  bnj106  34865  bnj125  34869  bnj154  34875  bnj155  34876  bnj526  34885  bnj540  34889  bnj609  34914  bnj611  34915  bnj893  34925  bnj1000  34938  bnj1014  34958  bnj1015  34959  bnj1234  35010  bnj1463  35052  gblacfnacd  35096  loop1cycl  35131  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  subfacp1  35180  sconnpht  35223  cnpconn  35224  txpconn  35226  ptpconn  35227  indispconn  35228  connpconn  35229  cvxpconn  35236  cvmliftmo  35278  cvmliftlem14  35291  cvmliftlem15  35292  cvmliftiota  35295  cvmlift2  35310  cvmliftphtlem  35311  cvmlift3lem2  35314  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  cvmlift3  35322  satfv1lem  35356  satfv1  35357  sategoelfvb  35413  mrsubff1  35508  mrsub0  35510  mrsubccat  35512  mrsubcn  35513  elmsubrn  35522  msubrn  35523  msubco  35525  msubvrs  35554  mclsax  35563  shftvalg  35726  fwddifval  36157  fwddifnval  36158  bj-evalval  37070  unceq  37598  matunitlindflem2  37618  poimirlem17  37638  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem27  37648  poimirlem28  37649  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  poimir  37654  broucube  37655  voliunnfl  37665  volsupnfl  37666  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  ftc1anclem2  37695  ftc1anclem5  37698  upixp  37730  fdc  37746  isismty  37802  rrnmval  37829  elghomlem2OLD  37887  isrngohom  37966  islfl  39060  isopos  39180  islaut  40084  ispautN  40100  isldil  40111  isltrn  40120  ltrnid  40136  ltrneq2  40149  isdilN  40155  istrnN  40158  trlval  40163  ltrneq3  40209  cdleme50ex  40560  cdleme  40561  cdlemg1a  40571  ltrniotaval  40582  ltrniotavalbN  40585  cdlemeiota  40586  cdlemg2jlemOLDN  40594  cdlemg2fvlem  40595  cdlemg2klem  40596  istendo  40761  tendoplcbv  40776  tendopl  40777  tendoicbv  40794  tendoi  40795  tendoid0  40826  tendo1ne0  40829  cdlemksv2  40848  cdlemkuv2  40868  cdlemk33N  40910  cdlemk34  40911  cdlemk36  40914  cdlemk19u  40971  cdlemk  40975  tendoex  40976  dvavsca  41018  dvhvscacbv  41099  dvhvscaval  41100  dicopelval  41178  dicelval1sta  41188  diclspsn  41195  dihmeetlem13N  41320  dih1dimatlem0  41329  dih1dimatlem  41330  dihpN  41337  islpolN  41484  hdmap1fval  41797  hdmapfval  41828  sticksstones1  42141  sticksstones2  42142  sticksstones3  42143  sticksstones8  42148  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones15  42156  frlmsnic  42535  uvcn0  42537  pwsgprod  42539  mplmapghm  42551  evlsvval  42555  evlsvvval  42558  evlsvarval  42560  evlsbagval  42561  selvvvval  42580  evlselv  42582  fsuppssindlem2  42587  fsuppssind  42588  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  sn-isghm  42668  ismrc  42696  mzpclval  42720  mzpsubst  42743  mzprename  42744  mzpcompact2lem  42746  eldioph  42753  eldioph2  42757  eldioph2b  42758  eldioph3  42761  rexrabdioph  42789  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  eldioph4i  42807  rabren3dioph  42810  mzpcong  42968  jm2.27dlem1  43005  wepwsolem  43038  aomclem6  43055  aomclem8  43057  dfac11  43058  dgraalem  43141  dgraaub  43144  dgraa0p  43145  mpaaeu  43146  mpaalem  43148  aaitgo  43158  rngunsnply  43165  cantnfresb  43320  tfsconcatun  43333  nvocnvb  43418  eliunov2  43675  rfovcnvfvd  44003  fsovfvd  44006  fsovcnvlem  44009  dssmapfv2d  44014  dssmapnvod  44016  clsk1independent  44042  ntrclskb  44065  ntrclsk13  44067  gneispace2  44128  mnringmulrvald  44223  dvconstbi  44330  addrval  44462  subrval  44463  mulvval  44464  relpeq1  44941  fnchoice  45030  refsum2cnlem1  45038  choicefi  45201  axccdom  45223  fmulcl  45586  fmuldfeqlem1  45587  mccllem  45602  mccl  45603  climf  45627  climf2  45671  dvnprodlem1  45951  dvnprodlem3  45953  dvnprod  45954  stoweidlem2  46007  stoweidlem6  46011  stoweidlem8  46013  stoweidlem9  46014  stoweidlem15  46020  stoweidlem16  46021  stoweidlem17  46022  stoweidlem18  46023  stoweidlem21  46026  stoweidlem27  46032  stoweidlem31  46036  stoweidlem36  46041  stoweidlem37  46042  stoweidlem41  46046  stoweidlem43  46048  stoweidlem44  46049  stoweidlem45  46050  stoweidlem46  46051  stoweidlem48  46053  stoweidlem51  46056  stoweidlem55  46060  stoweidlem59  46064  stoweidlem60  46065  stoweidlem62  46067  fourierdlem2  46114  fourierdlem3  46115  elaa2lem  46238  etransclem11  46250  etransclem24  46263  etransclem26  46265  etransclem28  46267  etransclem35  46274  rrndistlt  46295  ioorrnopn  46310  subsaliuncllem  46362  sge0val  46371  ismea  46456  caragenval  46498  isome  46499  isomenndlem  46535  hoicvrrex  46561  ovnlecvr  46563  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  ovnsubadd  46577  hsphoif  46581  hoidmvval  46582  hsphoival  46584  hoidmvlelem3  46602  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  ovncvr2  46616  hoidifhspval2  46620  hoiqssbllem2  46628  hspmbllem2  46632  hspmbllem3  46633  hspmbl  46634  ovnovollem1  46661  smfmullem2  46797  smfmul  46800  smfpimcclem  46812  tworepnotupword  46891  cfsetsnfsetfv  47062  cfsetsnfsetfo  47065  iccpart  47421  iccpartiun  47439  icceuelpart  47441  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbnd  47814  isisubgr  47866  isgrim  47886  grimidvtxedg  47889  grimcnv  47892  grimco  47893  isuspgrim0  47898  gricushgr  47921  ushggricedg  47931  uhgrimisgrgric  47935  isgrtri  47946  isubgr3stgrlem3  47971  isubgr3stgr  47978  isgrlim  47985  uspgrlim  47995  grlicref  48008  grlicsym  48009  grlictr  48011  isupwlk  48128  lincval  48402  lincdifsn  48417  linindslinci  48441  lindslinindsimp1  48450  linds0  48458  el0ldep  48459  lindsrng01  48461  snlindsntorlem  48463  ldepspr  48466  islindeps2  48476  zlmodzxzldep  48497  bigoval  48542  elbigo  48544  0aryfvalelfv  48628  1arympt1fv  48632  1arymaptfv  48633  1arymaptfo  48636  2arymptfv  48643  2arymaptfv  48644  2arymaptfo  48647  prelrrx2b  48707  rrx2plord  48713  rrx2vlinest  48734  rrx2linesl  48736  elrrx2linest2  48738  line2ylem  48744  line2xlem  48746  itsclc0  48764  itsclc0b  48765  itscnhlinecirc02p  48778  elfvne0  48841  iinfprg  49052  thincciso  49446  thinccisod  49447  setrecseq  49678  aacllem  49794