Theorem fveq1 6839

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 5104	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6483	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6507	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6507	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102  ℩cio 6450  ‘cfv 6499

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507

This theorem is referenced by:  fveq1i  6841  fveq1d  6842  iffv  6857  fvmptd3f  6965  fvmptdv2  6968  eqfnun  6991  fsnex  7240  f1prex  7241  isoeq1  7274  oveq  7375  elovmpt3imp  7626  ofrfvalg  7641  offval  7642  offval3  7940  bropopvvv  8046  bropfvvvvlem  8047  poseq  8114  soseq  8115  frrlem1  8242  frrlem13  8254  smoeq  8296  tfrlem12  8334  tz7.44-2  8352  tz7.44-3  8353  rdgeq1  8356  fsetfocdm  8811  fsetprcnex  8812  mapsncnv  8843  elixp2  8851  resixpfo  8886  elixpsn  8887  mapsnend  8984  enfixsn  9027  mapxpen  9084  ac6sfi  9207  ordtypelem7  9453  wemaplem1  9475  ixpiunwdom  9519  oemapval  9612  cantnf  9622  wemapwe  9626  cnfcom3clem  9634  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  updjud  9863  infxpenc2lem2  9949  fseqenlem1  9953  dfac8clem  9961  ac5num  9965  acni  9974  acni2  9975  acnlem  9977  dfac4  10051  dfac5lem5  10056  dfac2a  10059  dfac9  10066  dfacacn  10071  dfac12lem1  10073  dfac12r  10076  cofsmo  10198  cfsmolem  10199  cfsmo  10200  cfcoflem  10201  coftr  10202  alephsing  10205  isfin3ds  10258  fin23lem17  10267  fin23lem32  10273  fin23lem39  10279  isf33lem  10295  isf34lem6  10309  axcc2lem  10365  axcc3  10367  axdc2lem  10377  axdc3lem2  10380  axdc3lem3  10381  axdc3  10383  axdc4lem  10384  axcclem  10386  ac6num  10408  axdclem2  10449  konigthlem  10497  inar1  10704  1fv  13584  axdc4uzlem  13924  seqeq3  13947  seqof  14000  ccatfval  14514  wrdl1s1  14555  ccat1st1st  14569  cshf1  14751  cshweqrep  14762  wrdlen2i  14884  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  wrd2f1tovbij  14902  rtrclreclem1  14999  dfrtrclrec2  15000  rtrclreclem2  15001  rtrclreclem4  15003  dfrtrcl2  15004  clim  15436  rlim  15437  ello1  15457  elo1  15468  summo  15659  fsum  15662  prodmo  15878  fprod  15883  bpolylem  15990  bpolyval  15991  vdwlem6  16933  vdwlem8  16935  ramcl  16976  strfvnd  17131  prdsplusgval  17412  prdsmulrval  17414  prdsleval  17416  prdsdsval  17417  prdsvscaval  17418  xpsff1o  17506  isacs2  17590  isnat  17888  yonedalem3b  18216  yonedainv  18218  ismgmhm  18599  ismhm  18688  prdspjmhm  18732  isgrpinv  18901  pwsmulg  19027  isghm  19123  isghmOLD  19124  cayleylem2  19319  symgfix2  19322  gsmsymgrfix  19334  gsmsymgreq  19338  symgfixelq  19339  pmtr3ncomlem2  19380  pmtrdifel  19386  pmtrdifwrdel  19391  pmtrdifwrdel2  19392  psgnunilem2  19401  psgnunilem3  19402  efgsdm  19636  efgredlemd  19650  efgredlem  19653  efgred  19654  efgrelexlema  19655  efgrelexlemb  19656  prdsgsum  19887  pwspjmhmmgpd  20213  pwsexpg  20214  isrnghm  20326  isabv  20696  islmhm  20910  frgpcyg  21459  psgndiflemB  21485  psgndiflemA  21486  dsmmelbas  21624  frlmipval  21664  frlmphl  21666  uvcf1  21677  islindf  21697  islindf4  21723  psrmulfval  21828  evlslem2  21962  evlslem3  21963  evlslem1  21965  mpfrcl  21968  selvval  21998  psdval  22022  psdcoef  22023  psdadd  22026  psdmul  22029  psdmvr  22032  coe1fval  22066  coe1mul2lem2  22130  coe1tm  22135  madetsumid  22324  mvmulval  22406  marepvval0  22429  mulmarep1gsum2  22437  mdetleib2  22451  m1detdiag  22460  mdetralt  22471  mdetunilem7  22481  mdetunilem9  22483  m2detleiblem3  22492  m2detleiblem4  22493  m2detleib  22494  symgmatr01lem  22516  gsummatr01lem1  22518  gsummatr01lem4  22521  gsummatr01  22522  smadiadetlem3  22531  pmatcoe1fsupp  22564  pmatcollpw3lem  22646  pmatcollpw3fi1lem2  22650  iscnp  23100  1stcfb  23308  ptpjpre1  23434  elpt  23435  elptr  23436  ptpjopn  23475  dfac14  23481  upxp  23486  pthaus  23501  ptrescn  23502  xkoptsub  23517  cnmptkp  23543  xkofvcn  23547  cnmptk1p  23548  cnmptk2  23549  ptunhmeo  23671  ptcmplem3  23917  ptcmplem4  23918  symgtgp  23969  prdstmdd  23987  isucn  24141  imasdsf1olem  24237  prdsxmslem2  24393  tngngp3  24520  nmoval  24579  elcncf  24758  ishtpy  24847  pcoval  24887  om1elbas  24908  elpi1i  24922  iscau  25152  rrxds  25269  rrxdsfival  25289  ehl1eudisval  25297  ehl2eudisval  25299  mbfi1fseqlem6  25597  mbfi1flimlem  25599  isibl  25642  deg1ldg  25973  deg1leb  25976  elply2  26077  elplyr  26082  ne0p  26088  coeeu  26106  coelem  26107  coeeq  26108  coeidlem  26118  elqaalem3  26205  qaa  26207  iaa  26209  aareccl  26210  aannenlem2  26213  aaliou2  26224  dchrptlem2  27152  dchrpt  27154  dchrsum2  27155  sumdchr2  27157  dchrvmaeq0  27391  rpvmasum2  27399  dchrisum0re  27400  ostth  27526  sltval  27535  nolesgn2o  27559  nogesgn1o  27561  noresle  27585  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupfv  27594  noinfcbv  27605  noinffv  27609  iscgrg  28415  isismt  28437  israg  28600  iseqlg  28770  brbtwn  28802  brbtwn2  28808  colinearalg  28813  axsegconlem1  28820  axsegcon  28830  ax5seglem5  28836  axpasch  28844  axlowdim  28864  axeuclidlem  28865  axcontlem1  28867  axcontlem2  28868  axcontlem5  28871  vtxdgfval  29371  1egrvtxdg1  29413  isewlk  29506  iswlk  29514  uspgr2wlkeq2  29550  iswlkon  29559  isclwlk  29676  iscrct  29693  iscycl  29694  iswwlks  29739  wwlknon  29760  wlkiswwlks2  29778  wwlksnredwwlkn0  29799  wlksnwwlknvbij  29811  wwlksnextproplem3  29814  wwlksnextprop  29815  umgr2wlk  29852  midwwlks2s3  29855  elwwlks2  29869  elwspths2spth  29870  rusgrnumwwlkslem  29872  rusgrnumwwlkb0  29874  rusgrnumwwlks  29877  isclwwlk  29886  clwlkclwwlklem1  29901  clwwlkn1loopb  29945  clwwlkel  29948  clwwlkf  29949  clwwlkf1  29951  isclwwlknon  29993  clwwlknon1  29999  s2elclwwlknon2  30006  clwwlkvbij  30015  uhgr3cyclex  30084  fusgreg2wsplem  30235  fusgr2wsp2nb  30236  fusgreghash2wsp  30240  2clwwlkel  30251  extwwlkfabel  30255  numclwwlk1lem2fv  30258  numclwwlk1lem2  30262  clwwlknonclwlknonf1o  30264  dlwwlknondlwlknonf1o  30267  numclwwlk2lem1  30278  numclwlk2lem2f  30279  numclwlk2lem2f1o  30281  ex-fv  30345  isnvlem  30512  islno  30655  nmooval  30665  nmblolbi  30702  isphg  30719  ajmoi  30760  ajval  30763  ubthlem3  30774  htthlem  30819  hcau  31086  hlimi  31090  hosmval  31637  hommval  31638  hodmval  31639  hfsmval  31640  hfmmval  31641  adjmo  31734  nmopval  31758  elcnop  31759  ellnop  31760  elunop  31774  elhmop  31775  nmfnval  31778  elcnfn  31784  ellnfn  31785  adjeu  31791  adjval  31792  eigvecval  31798  eigvalfval  31799  adj1  31835  adjeq  31837  hmopadj2  31843  lnopeq0i  31909  lnopeq  31911  elunop2  31915  lnophm  31921  hmopco  31925  nmbdoplb  31927  nmcoplb  31932  lnopcon  31937  lnfn0  31949  lnfnmul  31950  nmbdfnlb  31952  nmcfnlb  31956  lnfncon  31958  riesz4  31966  riesz1  31967  cnlnadjlem9  31977  cnlnadjeu  31980  cnlnssadj  31982  nmopcoi  31997  bra11  32010  cnvbraval  32012  pjss2coi  32066  pjssdif2i  32076  pjssdif1i  32077  pjclem4  32101  pj3si  32109  pj3cor1i  32111  isst  32115  ishst  32116  stri  32159  hstri  32167  aciunf1lem  32559  ismnt  32882  mgcval  32886  ischn  32905  chnind  32910  chnub  32911  fzo0pmtrlast  33022  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  elrgspn  33170  elrgspnsubrunlem1  33171  linds2eq  33325  elrspunidl  33372  elrspunsn  33373  dfufd2lem  33493  lbsdiflsp0  33595  fedgmullem1  33598  fedgmullem2  33599  fedgmul  33600  fldextrspunlsplem  33641  fldextrspunlsp  33642  fldext2chn  33691  constrextdg2lem  33711  constrextdg2  33712  lmatval  33776  mdetpmtr1  33786  zarcmplem  33844  ismeas  34162  isrnmeas  34163  cntnevol  34191  carsgval  34267  sitgval  34296  eulerpartleme  34327  eulerpartlemd  34330  eulerpartlemr  34338  eulerpartlemgvv  34340  eulerpart  34346  cndprobval  34397  signstfvneq0  34536  reprsum  34577  reprsuc  34579  reprpmtf1o  34590  reprdifc  34591  breprexp  34597  vtsval  34601  hgt750lemb  34620  hgt750lema  34621  hgt750leme  34622  bnj66  34823  bnj106  34831  bnj125  34835  bnj154  34841  bnj155  34842  bnj526  34851  bnj540  34855  bnj609  34880  bnj611  34881  bnj893  34891  bnj1000  34904  bnj1014  34924  bnj1015  34925  bnj1234  34976  bnj1463  35018  gblacfnacd  35062  loop1cycl  35097  derangenlem  35131  subfacp1lem3  35142  subfacp1lem5  35144  subfacp1lem6  35145  subfacp1  35146  sconnpht  35189  cnpconn  35190  txpconn  35192  ptpconn  35193  indispconn  35194  connpconn  35195  cvxpconn  35202  cvmliftmo  35244  cvmliftlem14  35257  cvmliftlem15  35258  cvmliftiota  35261  cvmlift2  35276  cvmliftphtlem  35277  cvmlift3lem2  35280  cvmlift3lem6  35284  cvmlift3lem7  35285  cvmlift3lem9  35287  cvmlift3  35288  satfv1lem  35322  satfv1  35323  sategoelfvb  35379  mrsubff1  35474  mrsub0  35476  mrsubccat  35478  mrsubcn  35479  elmsubrn  35488  msubrn  35489  msubco  35491  msubvrs  35520  mclsax  35529  shftvalg  35692  fwddifval  36123  fwddifnval  36124  bj-evalval  37036  unceq  37564  matunitlindflem2  37584  poimirlem17  37604  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem27  37614  poimirlem28  37615  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  poimir  37620  broucube  37621  voliunnfl  37631  volsupnfl  37632  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  ftc1anclem2  37661  ftc1anclem5  37664  upixp  37696  fdc  37712  isismty  37768  rrnmval  37795  elghomlem2OLD  37853  isrngohom  37932  islfl  39026  isopos  39146  islaut  40050  ispautN  40066  isldil  40077  isltrn  40086  ltrnid  40102  ltrneq2  40115  isdilN  40121  istrnN  40124  trlval  40129  ltrneq3  40175  cdleme50ex  40526  cdleme  40527  cdlemg1a  40537  ltrniotaval  40548  ltrniotavalbN  40551  cdlemeiota  40552  cdlemg2jlemOLDN  40560  cdlemg2fvlem  40561  cdlemg2klem  40562  istendo  40727  tendoplcbv  40742  tendopl  40743  tendoicbv  40760  tendoi  40761  tendoid0  40792  tendo1ne0  40795  cdlemksv2  40814  cdlemkuv2  40834  cdlemk33N  40876  cdlemk34  40877  cdlemk36  40880  cdlemk19u  40937  cdlemk  40941  tendoex  40942  dvavsca  40984  dvhvscacbv  41065  dvhvscaval  41066  dicopelval  41144  dicelval1sta  41154  diclspsn  41161  dihmeetlem13N  41286  dih1dimatlem0  41295  dih1dimatlem  41296  dihpN  41303  islpolN  41450  hdmap1fval  41763  hdmapfval  41794  sticksstones1  42107  sticksstones2  42108  sticksstones3  42109  sticksstones8  42114  sticksstones10  42116  sticksstones11  42117  sticksstones12a  42118  sticksstones12  42119  sticksstones15  42122  frlmsnic  42501  uvcn0  42503  pwsgprod  42505  mplmapghm  42517  evlsvval  42521  evlsvvval  42524  evlsvarval  42526  evlsbagval  42527  selvvvval  42546  evlselv  42548  fsuppssindlem2  42553  fsuppssind  42554  prjspnfv01  42585  prjspner01  42586  prjspner1  42587  sn-isghm  42634  ismrc  42662  mzpclval  42686  mzpsubst  42709  mzprename  42710  mzpcompact2lem  42712  eldioph  42719  eldioph2  42723  eldioph2b  42724  eldioph3  42727  rexrabdioph  42755  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  eldioph4i  42773  rabren3dioph  42776  mzpcong  42934  jm2.27dlem1  42971  wepwsolem  43004  aomclem6  43021  aomclem8  43023  dfac11  43024  dgraalem  43107  dgraaub  43110  dgraa0p  43111  mpaaeu  43112  mpaalem  43114  aaitgo  43124  rngunsnply  43131  cantnfresb  43286  tfsconcatun  43299  nvocnvb  43384  eliunov2  43641  rfovcnvfvd  43969  fsovfvd  43972  fsovcnvlem  43975  dssmapfv2d  43980  dssmapnvod  43982  clsk1independent  44008  ntrclskb  44031  ntrclsk13  44033  gneispace2  44094  mnringmulrvald  44189  dvconstbi  44296  addrval  44428  subrval  44429  mulvval  44430  relpeq1  44907  fnchoice  44996  refsum2cnlem1  45004  choicefi  45167  axccdom  45189  fmulcl  45552  fmuldfeqlem1  45553  mccllem  45568  mccl  45569  climf  45593  climf2  45637  dvnprodlem1  45917  dvnprodlem3  45919  dvnprod  45920  stoweidlem2  45973  stoweidlem6  45977  stoweidlem8  45979  stoweidlem9  45980  stoweidlem15  45986  stoweidlem16  45987  stoweidlem17  45988  stoweidlem18  45989  stoweidlem21  45992  stoweidlem27  45998  stoweidlem31  46002  stoweidlem36  46007  stoweidlem37  46008  stoweidlem41  46012  stoweidlem43  46014  stoweidlem44  46015  stoweidlem45  46016  stoweidlem46  46017  stoweidlem48  46019  stoweidlem51  46022  stoweidlem55  46026  stoweidlem59  46030  stoweidlem60  46031  stoweidlem62  46033  fourierdlem2  46080  fourierdlem3  46081  elaa2lem  46204  etransclem11  46216  etransclem24  46229  etransclem26  46231  etransclem28  46233  etransclem35  46240  rrndistlt  46261  ioorrnopn  46276  subsaliuncllem  46328  sge0val  46337  ismea  46422  caragenval  46464  isome  46465  isomenndlem  46501  hoicvrrex  46527  ovnlecvr  46529  ovncvrrp  46535  ovn0lem  46536  ovnsubaddlem1  46541  ovnsubadd  46543  hsphoif  46547  hoidmvval  46548  hsphoival  46550  hoidmvlelem3  46568  hoidmvlelem5  46570  hoidmvle  46571  ovnhoilem1  46572  ovnhoi  46574  ovnlecvr2  46581  ovncvr2  46582  hoidifhspval2  46586  hoiqssbllem2  46594  hspmbllem2  46598  hspmbllem3  46599  hspmbl  46600  ovnovollem1  46627  smfmullem2  46763  smfmul  46766  smfpimcclem  46778  tworepnotupword  46857  sinnpoly  46865  cfsetsnfsetfv  47031  cfsetsnfsetfo  47034  iccpart  47390  iccpartiun  47408  icceuelpart  47410  nnsum3primes4  47762  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  bgoldbtbnd  47783  isisubgr  47835  isgrim  47855  grimidvtxedg  47858  grimcnv  47861  grimco  47862  isuspgrim0  47867  gricushgr  47890  ushggricedg  47900  uhgrimisgrgric  47904  isgrtri  47915  isubgr3stgrlem3  47940  isubgr3stgr  47947  isgrlim  47954  uspgrlim  47964  grlicref  47977  grlicsym  47978  grlictr  47980  isupwlk  48097  lincval  48371  lincdifsn  48386  linindslinci  48410  lindslinindsimp1  48419  linds0  48427  el0ldep  48428  lindsrng01  48430  snlindsntorlem  48432  ldepspr  48435  islindeps2  48445  zlmodzxzldep  48466  bigoval  48511  elbigo  48513  0aryfvalelfv  48597  1arympt1fv  48601  1arymaptfv  48602  1arymaptfo  48605  2arymptfv  48612  2arymaptfv  48613  2arymaptfo  48616  prelrrx2b  48676  rrx2plord  48682  rrx2vlinest  48703  rrx2linesl  48705  elrrx2linest2  48707  line2ylem  48713  line2xlem  48715  itsclc0  48733  itsclc0b  48734  itscnhlinecirc02p  48747  elfvne0  48810  iinfprg  49021  thincciso  49415  thinccisod  49416  setrecseq  49647  aacllem  49763