Theorem fveq1 6846

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 6485	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6509	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6509	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5110  ℩cio 6451  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509

This theorem is referenced by:  fveq1i  6848  fveq1d  6849  iffv  6864  fvmptd3f  6968  fvmptdv2  6971  fsnex  7234  f1prex  7235  isoeq1  7267  oveq  7368  elovmpt3imp  7615  ofrfvalg  7630  offval  7631  offval3  7920  bropopvvv  8027  bropfvvvvlem  8028  poseq  8095  soseq  8096  frrlem1  8222  frrlem13  8234  wfrlem1OLD  8259  wfrlem3OLDa  8262  wfrlem15OLD  8274  smoeq  8301  tfrlem12  8340  tz7.44-2  8358  tz7.44-3  8359  rdgeq1  8362  fsetfocdm  8806  fsetprcnex  8807  mapsncnv  8838  elixp2  8846  resixpfo  8881  elixpsn  8882  mapsnend  8987  enfixsn  9032  mapxpen  9094  ac6sfi  9238  ordtypelem7  9469  wemaplem1  9491  ixpiunwdom  9535  oemapval  9628  cantnf  9638  wemapwe  9642  cnfcom3clem  9650  ssttrcl  9660  ttrcltr  9661  ttrclss  9665  ttrclselem2  9671  updjud  9879  infxpenc2lem2  9965  fseqenlem1  9969  dfac8clem  9977  ac5num  9981  acni  9990  acni2  9991  acnlem  9993  dfac4  10067  dfac5lem5  10072  dfac2a  10074  dfac9  10081  dfacacn  10086  dfac12lem1  10088  dfac12r  10091  cofsmo  10214  cfsmolem  10215  cfsmo  10216  cfcoflem  10217  coftr  10218  alephsing  10221  isfin3ds  10274  fin23lem17  10283  fin23lem32  10289  fin23lem39  10295  isf33lem  10311  isf34lem6  10325  axcc2lem  10381  axcc3  10383  axdc2lem  10393  axdc3lem2  10396  axdc3lem3  10397  axdc3  10399  axdc4lem  10400  axcclem  10402  ac6num  10424  axdclem2  10465  konigthlem  10513  inar1  10720  1fv  13570  axdc4uzlem  13898  seqeq3  13921  seqof  13975  ccatfval  14473  wrdl1s1  14514  ccat1st1st  14528  cshf1  14710  cshweqrep  14721  wrdlen2i  14843  wwlktovf  14857  wwlktovf1  14858  wwlktovfo  14859  wrd2f1tovbij  14861  rtrclreclem1  14954  dfrtrclrec2  14955  rtrclreclem2  14956  rtrclreclem4  14958  dfrtrcl2  14959  clim  15388  rlim  15389  ello1  15409  elo1  15420  summo  15613  fsum  15616  prodmo  15830  fprod  15835  bpolylem  15942  bpolyval  15943  vdwlem6  16869  vdwlem8  16871  ramcl  16912  strfvnd  17068  prdsplusgval  17369  prdsmulrval  17371  prdsleval  17373  prdsdsval  17374  prdsvscaval  17375  xpsff1o  17463  isacs2  17547  isnat  17848  yonedalem3b  18182  yonedainv  18184  ismhm  18617  prdspjmhm  18653  isgrpinv  18818  pwsmulg  18935  isghm  19022  cayleylem2  19209  symgfix2  19212  gsmsymgrfix  19224  gsmsymgreq  19228  symgfixelq  19229  pmtr3ncomlem2  19270  pmtrdifel  19276  pmtrdifwrdel  19281  pmtrdifwrdel2  19282  psgnunilem2  19291  psgnunilem3  19292  efgsdm  19526  efgredlemd  19540  efgredlem  19543  efgred  19544  efgrelexlema  19545  efgrelexlemb  19546  prdsgsum  19772  pwspjmhmmgpd  20057  pwsexpg  20058  isabv  20334  islmhm  20545  frgpcyg  21017  psgndiflemB  21041  psgndiflemA  21042  dsmmelbas  21182  frlmipval  21222  frlmphl  21224  uvcf1  21235  islindf  21255  islindf4  21281  psrmulfval  21390  evlslem2  21526  evlslem3  21527  evlslem1  21529  mpfrcl  21532  selvval  21565  coe1fval  21613  coe1mul2lem2  21676  coe1tm  21681  madetsumid  21847  mvmulval  21929  marepvval0  21952  mulmarep1gsum2  21960  mdetleib2  21974  m1detdiag  21983  mdetralt  21994  mdetunilem7  22004  mdetunilem9  22006  m2detleiblem3  22015  m2detleiblem4  22016  m2detleib  22017  symgmatr01lem  22039  gsummatr01lem1  22041  gsummatr01lem4  22044  gsummatr01  22045  smadiadetlem3  22054  pmatcoe1fsupp  22087  pmatcollpw3lem  22169  pmatcollpw3fi1lem2  22173  iscnp  22625  1stcfb  22833  ptpjpre1  22959  elpt  22960  elptr  22961  ptpjopn  23000  dfac14  23006  upxp  23011  pthaus  23026  ptrescn  23027  xkoptsub  23042  cnmptkp  23068  xkofvcn  23072  cnmptk1p  23073  cnmptk2  23074  ptunhmeo  23196  ptcmplem3  23442  ptcmplem4  23443  symgtgp  23494  prdstmdd  23512  isucn  23667  imasdsf1olem  23763  prdsxmslem2  23922  tngngp3  24057  nmoval  24116  elcncf  24289  ishtpy  24372  pcoval  24411  om1elbas  24432  elpi1i  24446  iscau  24677  rrxds  24794  rrxdsfival  24814  ehl1eudisval  24822  ehl2eudisval  24824  mbfi1fseqlem6  25122  mbfi1flimlem  25124  isibl  25167  deg1ldg  25494  deg1leb  25497  elply2  25594  elplyr  25599  ne0p  25605  coeeu  25623  coelem  25624  coeeq  25625  coeidlem  25635  elqaalem3  25718  qaa  25720  iaa  25722  aareccl  25723  aannenlem2  25726  aaliou2  25737  dchrptlem2  26650  dchrpt  26652  dchrsum2  26653  sumdchr2  26655  dchrvmaeq0  26889  rpvmasum2  26897  dchrisum0re  26898  ostth  27024  sltval  27032  nolesgn2o  27056  nogesgn1o  27058  noresle  27082  nosupprefixmo  27085  noinfprefixmo  27086  nosupcbv  27087  nosupfv  27091  noinfcbv  27102  noinffv  27106  iscgrg  27517  isismt  27539  israg  27702  iseqlg  27872  brbtwn  27911  brbtwn2  27917  colinearalg  27922  axsegconlem1  27929  axsegcon  27939  ax5seglem5  27945  axpasch  27953  axlowdim  27973  axeuclidlem  27974  axcontlem1  27976  axcontlem2  27977  axcontlem5  27980  vtxdgfval  28478  1egrvtxdg1  28520  isewlk  28613  iswlk  28621  uspgr2wlkeq2  28658  iswlkon  28668  isclwlk  28784  iscrct  28801  iscycl  28802  iswwlks  28844  wwlknon  28865  wlkiswwlks2  28883  wwlksnredwwlkn0  28904  wlksnwwlknvbij  28916  wwlksnextproplem3  28919  wwlksnextprop  28920  umgr2wlk  28957  midwwlks2s3  28960  elwwlks2  28974  elwspths2spth  28975  rusgrnumwwlkslem  28977  rusgrnumwwlkb0  28979  rusgrnumwwlks  28982  isclwwlk  28991  clwlkclwwlklem1  29006  clwwlkn1loopb  29050  clwwlkel  29053  clwwlkf  29054  clwwlkf1  29056  isclwwlknon  29098  clwwlknon1  29104  s2elclwwlknon2  29111  clwwlkvbij  29120  uhgr3cyclex  29189  fusgreg2wsplem  29340  fusgr2wsp2nb  29341  fusgreghash2wsp  29345  2clwwlkel  29356  extwwlkfabel  29360  numclwwlk1lem2fv  29363  numclwwlk1lem2  29367  clwwlknonclwlknonf1o  29369  dlwwlknondlwlknonf1o  29372  numclwwlk2lem1  29383  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  ex-fv  29450  isnvlem  29615  islno  29758  nmooval  29768  nmblolbi  29805  isphg  29822  ajmoi  29863  ajval  29866  ubthlem3  29877  htthlem  29922  hcau  30189  hlimi  30193  hosmval  30740  hommval  30741  hodmval  30742  hfsmval  30743  hfmmval  30744  adjmo  30837  nmopval  30861  elcnop  30862  ellnop  30863  elunop  30877  elhmop  30878  nmfnval  30881  elcnfn  30887  ellnfn  30888  adjeu  30894  adjval  30895  eigvecval  30901  eigvalfval  30902  adj1  30938  adjeq  30940  hmopadj2  30946  lnopeq0i  31012  lnopeq  31014  elunop2  31018  lnophm  31024  hmopco  31028  nmbdoplb  31030  nmcoplb  31035  lnopcon  31040  lnfn0  31052  lnfnmul  31053  nmbdfnlb  31055  nmcfnlb  31059  lnfncon  31061  riesz4  31069  riesz1  31070  cnlnadjlem9  31080  cnlnadjeu  31083  cnlnssadj  31085  nmopcoi  31100  bra11  31113  cnvbraval  31115  pjss2coi  31169  pjssdif2i  31179  pjssdif1i  31180  pjclem4  31204  pj3si  31212  pj3cor1i  31214  isst  31218  ishst  31219  stri  31262  hstri  31270  aciunf1lem  31645  ismnt  31913  mgcval  31917  linds2eq  32241  elrspunidl  32279  lbsdiflsp0  32408  fedgmullem1  32411  fedgmullem2  32412  fedgmul  32413  lmatval  32483  mdetpmtr1  32493  zarcmplem  32551  ismeas  32887  isrnmeas  32888  cntnevol  32916  carsgval  32992  sitgval  33021  eulerpartleme  33052  eulerpartlemd  33055  eulerpartlemr  33063  eulerpartlemgvv  33065  eulerpart  33071  cndprobval  33122  signstfvneq0  33273  reprsum  33315  reprsuc  33317  reprpmtf1o  33328  reprdifc  33329  breprexp  33335  vtsval  33339  hgt750lemb  33358  hgt750lema  33359  hgt750leme  33360  bnj66  33561  bnj106  33569  bnj125  33573  bnj154  33579  bnj155  33580  bnj526  33589  bnj540  33593  bnj609  33618  bnj611  33619  bnj893  33629  bnj1000  33642  bnj1014  33662  bnj1015  33663  bnj1234  33714  bnj1463  33756  loop1cycl  33818  derangenlem  33852  subfacp1lem3  33863  subfacp1lem5  33865  subfacp1lem6  33866  subfacp1  33867  sconnpht  33910  cnpconn  33911  txpconn  33913  ptpconn  33914  indispconn  33915  connpconn  33916  cvxpconn  33923  cvmliftmo  33965  cvmliftlem14  33978  cvmliftlem15  33979  cvmliftiota  33982  cvmlift2  33997  cvmliftphtlem  33998  cvmlift3lem2  34001  cvmlift3lem6  34005  cvmlift3lem7  34006  cvmlift3lem9  34008  cvmlift3  34009  satfv1lem  34043  satfv1  34044  sategoelfvb  34100  mrsubff1  34195  mrsub0  34197  mrsubccat  34199  mrsubcn  34200  elmsubrn  34209  msubrn  34210  msubco  34212  msubvrs  34241  mclsax  34250  shftvalg  34390  fwddifval  34823  fwddifnval  34824  bj-evalval  35619  unceq  36128  matunitlindflem2  36148  poimirlem17  36168  poimirlem20  36171  poimirlem22  36173  poimirlem23  36174  poimirlem27  36178  poimirlem28  36179  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  poimir  36184  broucube  36185  voliunnfl  36195  volsupnfl  36196  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  ftc1anclem2  36225  ftc1anclem5  36228  eqfnun  36254  upixp  36261  fdc  36277  isismty  36333  rrnmval  36360  elghomlem2OLD  36418  isrngohom  36497  islfl  37595  isopos  37715  islaut  38619  ispautN  38635  isldil  38646  isltrn  38655  ltrnid  38671  ltrneq2  38684  isdilN  38690  istrnN  38693  trlval  38698  ltrneq3  38744  cdleme50ex  39095  cdleme  39096  cdlemg1a  39106  ltrniotaval  39117  ltrniotavalbN  39120  cdlemeiota  39121  cdlemg2jlemOLDN  39129  cdlemg2fvlem  39130  cdlemg2klem  39131  istendo  39296  tendoplcbv  39311  tendopl  39312  tendoicbv  39329  tendoi  39330  tendoid0  39361  tendo1ne0  39364  cdlemksv2  39383  cdlemkuv2  39403  cdlemk33N  39445  cdlemk34  39446  cdlemk36  39449  cdlemk19u  39506  cdlemk  39510  tendoex  39511  dvavsca  39553  dvhvscacbv  39634  dvhvscaval  39635  dicopelval  39713  dicelval1sta  39723  diclspsn  39730  dihmeetlem13N  39855  dih1dimatlem0  39864  dih1dimatlem  39865  dihpN  39872  islpolN  40019  hdmap1fval  40332  hdmapfval  40363  sticksstones1  40627  sticksstones2  40628  sticksstones3  40629  sticksstones8  40634  sticksstones10  40636  sticksstones11  40637  sticksstones12a  40638  sticksstones12  40639  sticksstones15  40642  frlmsnic  40786  uvcn0  40788  pwsgprod  40790  evlsvval  40803  evlsvarval  40805  evlsbagval  40806  fsuppssindlem2  40825  fsuppssind  40826  prjspnfv01  41020  prjspner01  41021  prjspner1  41022  ismrc  41082  mzpclval  41106  mzpsubst  41129  mzprename  41130  mzpcompact2lem  41132  eldioph  41139  eldioph2  41143  eldioph2b  41144  eldioph3  41147  rexrabdioph  41175  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  eldioph4i  41193  rabren3dioph  41196  mzpcong  41354  jm2.27dlem1  41391  wepwsolem  41427  aomclem6  41444  aomclem8  41446  dfac11  41447  dgraalem  41530  dgraaub  41533  dgraa0p  41534  mpaaeu  41535  mpaalem  41537  aaitgo  41547  rngunsnply  41558  cantnfresb  41717  tfsconcatun  41730  nvocnvb  41816  eliunov2  42073  rfovcnvfvd  42401  fsovfvd  42404  fsovcnvlem  42407  dssmapfv2d  42412  dssmapnvod  42414  clsk1independent  42440  ntrclskb  42463  ntrclsk13  42465  gneispace2  42526  mnringmulrvald  42629  dvconstbi  42736  addrval  42868  subrval  42869  mulvval  42870  fnchoice  43356  refsum2cnlem1  43364  choicefi  43542  axccdom  43564  fmulcl  43942  fmuldfeqlem1  43943  mccllem  43958  mccl  43959  climf  43983  climf2  44027  dvnprodlem1  44307  dvnprodlem3  44309  dvnprod  44310  stoweidlem2  44363  stoweidlem6  44367  stoweidlem8  44369  stoweidlem9  44370  stoweidlem15  44376  stoweidlem16  44377  stoweidlem17  44378  stoweidlem18  44379  stoweidlem21  44382  stoweidlem27  44388  stoweidlem31  44392  stoweidlem36  44397  stoweidlem37  44398  stoweidlem41  44402  stoweidlem43  44404  stoweidlem44  44405  stoweidlem45  44406  stoweidlem46  44407  stoweidlem48  44409  stoweidlem51  44412  stoweidlem55  44416  stoweidlem59  44420  stoweidlem60  44421  stoweidlem62  44423  fourierdlem2  44470  fourierdlem3  44471  elaa2lem  44594  etransclem11  44606  etransclem24  44619  etransclem26  44621  etransclem28  44623  etransclem35  44630  rrndistlt  44651  ioorrnopn  44666  subsaliuncllem  44718  sge0val  44727  ismea  44812  caragenval  44854  isome  44855  isomenndlem  44891  hoicvrrex  44917  ovnlecvr  44919  ovncvrrp  44925  ovn0lem  44926  ovnsubaddlem1  44931  ovnsubadd  44933  hsphoif  44937  hoidmvval  44938  hsphoival  44940  hoidmvlelem3  44958  hoidmvlelem5  44960  hoidmvle  44961  ovnhoilem1  44962  ovnhoi  44964  ovnlecvr2  44971  ovncvr2  44972  hoidifhspval2  44976  hoiqssbllem2  44984  hspmbllem2  44988  hspmbllem3  44989  hspmbl  44990  ovnovollem1  45017  smfmullem2  45153  smfmul  45156  smfpimcclem  45168  tworepnotupword  45245  cfsetsnfsetfv  45411  cfsetsnfsetfo  45414  iccpart  45728  iccpartiun  45746  icceuelpart  45748  nnsum3primes4  46100  nnsum3primesgbe  46104  nnsum4primesodd  46108  nnsum4primesoddALTV  46109  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  bgoldbtbnd  46121  isomgreqve  46137  isomushgr  46138  isomuspgrlem2  46145  isomgrsym  46148  isomgrtr  46151  ushrisomgr  46153  isupwlk  46158  ismgmhm  46197  isrnghm  46310  lincval  46610  lincdifsn  46625  linindslinci  46649  lindslinindsimp1  46658  linds0  46666  el0ldep  46667  lindsrng01  46669  snlindsntorlem  46671  ldepspr  46674  islindeps2  46684  zlmodzxzldep  46705  bigoval  46755  elbigo  46757  0aryfvalelfv  46841  1arympt1fv  46845  1arymaptfv  46846  1arymaptfo  46849  2arymptfv  46856  2arymaptfv  46857  2arymaptfo  46860  prelrrx2b  46920  rrx2plord  46926  rrx2vlinest  46947  rrx2linesl  46949  elrrx2linest2  46951  line2ylem  46957  line2xlem  46959  itsclc0  46977  itsclc0b  46978  itscnhlinecirc02p  46991  elfvne0  47035  thincciso  47189  setrecseq  47250  aacllem  47368