Theorem fveq1 6841

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 5102	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6484	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6508	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6508	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100  ℩cio 6454  ‘cfv 6500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508

This theorem is referenced by:  fveq1i  6843  fveq1d  6844  iffv  6859  fvmptd3f  6965  fvmptdv2  6968  eqfnun  6991  fsnex  7239  f1prex  7240  isoeq1  7273  oveq  7374  elovmpt3imp  7625  ofrfvalg  7640  offval  7641  offval3  7936  bropopvvv  8042  bropfvvvvlem  8043  poseq  8110  soseq  8111  frrlem1  8238  frrlem13  8250  smoeq  8292  tfrlem12  8330  tz7.44-2  8348  tz7.44-3  8349  rdgeq1  8352  fsetfocdm  8810  fsetprcnex  8811  mapsncnv  8843  elixp2  8851  resixpfo  8886  elixpsn  8887  mapsnend  8985  enfixsn  9026  mapxpen  9083  ac6sfi  9196  ordtypelem7  9441  wemaplem1  9463  ixpiunwdom  9507  oemapval  9604  cantnf  9614  wemapwe  9618  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  updjud  9858  infxpenc2lem2  9942  fseqenlem1  9946  dfac8clem  9954  ac5num  9958  acni  9967  acni2  9968  acnlem  9970  dfac4  10044  dfac5lem5  10049  dfac2a  10052  dfac9  10059  dfacacn  10064  dfac12lem1  10066  dfac12r  10069  cofsmo  10191  cfsmolem  10192  cfsmo  10193  cfcoflem  10194  coftr  10195  alephsing  10198  isfin3ds  10251  fin23lem17  10260  fin23lem32  10266  fin23lem39  10272  isf33lem  10288  isf34lem6  10302  axcc2lem  10358  axcc3  10360  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3  10376  axdc4lem  10377  axcclem  10379  ac6num  10401  axdclem2  10442  konigthlem  10491  inar1  10698  1fv  13575  axdc4uzlem  13918  seqeq3  13941  seqof  13994  ccatfval  14508  wrdl1s1  14550  ccat1st1st  14564  cshf1  14745  cshweqrep  14756  wrdlen2i  14877  wwlktovf  14891  wwlktovf1  14892  wwlktovfo  14893  wrd2f1tovbij  14895  rtrclreclem1  14992  dfrtrclrec2  14993  rtrclreclem2  14994  rtrclreclem4  14996  dfrtrcl2  14997  clim  15429  rlim  15430  ello1  15450  elo1  15461  summo  15652  fsum  15655  prodmo  15871  fprod  15876  bpolylem  15983  bpolyval  15984  vdwlem6  16926  vdwlem8  16928  ramcl  16969  strfvnd  17124  prdsplusgval  17405  prdsmulrval  17407  prdsleval  17409  prdsdsval  17410  prdsvscaval  17411  xpsff1o  17500  isacs2  17588  isnat  17886  yonedalem3b  18214  yonedainv  18216  ischn  18542  chnind  18556  chnub  18557  ismgmhm  18633  ismhm  18722  prdspjmhm  18766  isgrpinv  18935  pwsmulg  19061  isghm  19156  isghmOLD  19157  cayleylem2  19354  symgfix2  19357  gsmsymgrfix  19369  gsmsymgreq  19373  symgfixelq  19374  pmtr3ncomlem2  19415  pmtrdifel  19421  pmtrdifwrdel  19426  pmtrdifwrdel2  19427  psgnunilem2  19436  psgnunilem3  19437  efgsdm  19671  efgredlemd  19685  efgredlem  19688  efgred  19689  efgrelexlema  19690  efgrelexlemb  19691  prdsgsum  19922  pwspjmhmmgpd  20275  pwsexpg  20276  pwsgprod  20277  isrnghm  20389  isabv  20756  islmhm  20991  frgpcyg  21540  psgndiflemB  21567  psgndiflemA  21568  dsmmelbas  21706  frlmipval  21746  frlmphl  21748  uvcf1  21759  islindf  21779  islindf4  21805  psrmulfval  21911  evlslem2  22046  evlslem3  22047  evlslem1  22049  mpfrcl  22052  evlsvval  22057  evlsvvval  22060  selvval  22090  psdval  22114  psdcoef  22115  psdadd  22118  psdmul  22121  psdmvr  22124  coe1fval  22158  coe1mul2lem2  22222  coe1tm  22227  madetsumid  22417  mvmulval  22499  marepvval0  22522  mulmarep1gsum2  22530  mdetleib2  22544  m1detdiag  22553  mdetralt  22564  mdetunilem7  22574  mdetunilem9  22576  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  symgmatr01lem  22609  gsummatr01lem1  22611  gsummatr01lem4  22614  gsummatr01  22615  smadiadetlem3  22624  pmatcoe1fsupp  22657  pmatcollpw3lem  22739  pmatcollpw3fi1lem2  22743  iscnp  23193  1stcfb  23401  ptpjpre1  23527  elpt  23528  elptr  23529  ptpjopn  23568  dfac14  23574  upxp  23579  pthaus  23594  ptrescn  23595  xkoptsub  23610  cnmptkp  23636  xkofvcn  23640  cnmptk1p  23641  cnmptk2  23642  ptunhmeo  23764  ptcmplem3  24010  ptcmplem4  24011  symgtgp  24062  prdstmdd  24080  isucn  24233  imasdsf1olem  24329  prdsxmslem2  24485  tngngp3  24612  nmoval  24671  elcncf  24850  ishtpy  24939  pcoval  24979  om1elbas  25000  elpi1i  25014  iscau  25244  rrxds  25361  rrxdsfival  25381  ehl1eudisval  25389  ehl2eudisval  25391  mbfi1fseqlem6  25689  mbfi1flimlem  25691  isibl  25734  deg1ldg  26065  deg1leb  26068  elply2  26169  elplyr  26174  ne0p  26180  coeeu  26198  coelem  26199  coeeq  26200  coeidlem  26210  elqaalem3  26297  qaa  26299  iaa  26301  aareccl  26302  aannenlem2  26305  aaliou2  26316  dchrptlem2  27244  dchrpt  27246  dchrsum2  27247  sumdchr2  27249  dchrvmaeq0  27483  rpvmasum2  27491  dchrisum0re  27492  ostth  27618  ltsval  27627  nolesgn2o  27651  nogesgn1o  27653  noresle  27677  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupfv  27686  noinfcbv  27697  noinffv  27701  iscgrg  28596  isismt  28618  israg  28781  iseqlg  28951  brbtwn  28984  brbtwn2  28990  colinearalg  28995  axsegconlem1  29002  axsegcon  29012  ax5seglem5  29018  axpasch  29026  axlowdim  29046  axeuclidlem  29047  axcontlem1  29049  axcontlem2  29050  axcontlem5  29053  vtxdgfval  29553  1egrvtxdg1  29595  isewlk  29688  iswlk  29696  uspgr2wlkeq2  29732  iswlkon  29741  isclwlk  29858  iscrct  29875  iscycl  29876  iswwlks  29921  wwlknon  29942  wlkiswwlks2  29960  wwlksnredwwlkn0  29981  wlksnwwlknvbij  29993  wwlksnextproplem3  29996  wwlksnextprop  29997  umgr2wlk  30034  midwwlks2s3  30037  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlkslem  30057  rusgrnumwwlkb0  30059  rusgrnumwwlks  30062  isclwwlk  30071  clwlkclwwlklem1  30086  clwwlkn1loopb  30130  clwwlkel  30133  clwwlkf  30134  clwwlkf1  30136  isclwwlknon  30178  clwwlknon1  30184  s2elclwwlknon2  30191  clwwlkvbij  30200  uhgr3cyclex  30269  fusgreg2wsplem  30420  fusgr2wsp2nb  30421  fusgreghash2wsp  30425  2clwwlkel  30436  extwwlkfabel  30440  numclwwlk1lem2fv  30443  numclwwlk1lem2  30447  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  ex-fv  30530  isnvlem  30698  islno  30841  nmooval  30851  nmblolbi  30888  isphg  30905  ajmoi  30946  ajval  30949  ubthlem3  30960  htthlem  31005  hcau  31272  hlimi  31276  hosmval  31823  hommval  31824  hodmval  31825  hfsmval  31826  hfmmval  31827  adjmo  31920  nmopval  31944  elcnop  31945  ellnop  31946  elunop  31960  elhmop  31961  nmfnval  31964  elcnfn  31970  ellnfn  31971  adjeu  31977  adjval  31978  eigvecval  31984  eigvalfval  31985  adj1  32021  adjeq  32023  hmopadj2  32029  lnopeq0i  32095  lnopeq  32097  elunop2  32101  lnophm  32107  hmopco  32111  nmbdoplb  32113  nmcoplb  32118  lnopcon  32123  lnfn0  32135  lnfnmul  32136  nmbdfnlb  32138  nmcfnlb  32142  lnfncon  32144  riesz4  32152  riesz1  32153  cnlnadjlem9  32163  cnlnadjeu  32166  cnlnssadj  32168  nmopcoi  32183  bra11  32196  cnvbraval  32198  pjss2coi  32252  pjssdif2i  32262  pjssdif1i  32263  pjclem4  32287  pj3si  32295  pj3cor1i  32297  isst  32301  ishst  32302  stri  32345  hstri  32353  aciunf1lem  32752  ismnt  33076  mgcval  33080  fzo0pmtrlast  33186  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem3  33338  elrgspnlem4  33339  elrgspn  33340  elrgspnsubrunlem1  33341  linds2eq  33474  elrspunidl  33521  elrspunsn  33522  dfufd2lem  33642  extvfv  33710  extvfvv  33711  extvfvcl  33713  evlvarval  33718  evlextv  33719  mplvrpmga  33722  splysubrg  33737  issply  33738  vietalem  33756  vieta  33757  lbsdiflsp0  33804  fedgmullem1  33807  fedgmullem2  33808  fedgmul  33809  fldextrspunlsplem  33851  fldextrspunlsp  33852  fldext2chn  33906  constrextdg2lem  33926  constrextdg2  33927  lmatval  33991  mdetpmtr1  34001  zarcmplem  34059  ismeas  34377  isrnmeas  34378  cntnevol  34406  carsgval  34481  sitgval  34510  eulerpartleme  34541  eulerpartlemd  34544  eulerpartlemr  34552  eulerpartlemgvv  34554  eulerpart  34560  cndprobval  34611  signstfvneq0  34750  reprsum  34791  reprsuc  34793  reprpmtf1o  34804  reprdifc  34805  breprexp  34811  vtsval  34815  hgt750lemb  34834  hgt750lema  34835  hgt750leme  34836  bnj66  35036  bnj106  35044  bnj125  35048  bnj154  35054  bnj155  35055  bnj526  35064  bnj540  35068  bnj609  35093  bnj611  35094  bnj893  35104  bnj1000  35117  bnj1014  35137  bnj1015  35138  bnj1234  35189  bnj1463  35231  fineqvnttrclse  35302  gblacfnacd  35318  loop1cycl  35353  derangenlem  35387  subfacp1lem3  35398  subfacp1lem5  35400  subfacp1lem6  35401  subfacp1  35402  sconnpht  35445  cnpconn  35446  txpconn  35448  ptpconn  35449  indispconn  35450  connpconn  35451  cvxpconn  35458  cvmliftmo  35500  cvmliftlem14  35513  cvmliftlem15  35514  cvmliftiota  35517  cvmlift2  35532  cvmliftphtlem  35533  cvmlift3lem2  35536  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  cvmlift3  35544  satfv1lem  35578  satfv1  35579  sategoelfvb  35635  mrsubff1  35730  mrsub0  35732  mrsubccat  35734  mrsubcn  35735  elmsubrn  35744  msubrn  35745  msubco  35747  msubvrs  35776  mclsax  35785  shftvalg  35948  fwddifval  36378  fwddifnval  36379  bj-evalval  37328  unceq  37848  matunitlindflem2  37868  poimirlem17  37888  poimirlem20  37891  poimirlem22  37893  poimirlem23  37894  poimirlem27  37898  poimirlem28  37899  poimirlem30  37901  poimirlem31  37902  poimirlem32  37903  poimir  37904  broucube  37905  voliunnfl  37915  volsupnfl  37916  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  ftc1anclem2  37945  ftc1anclem5  37948  upixp  37980  fdc  37996  isismty  38052  rrnmval  38079  elghomlem2OLD  38137  isrngohom  38216  islfl  39436  isopos  39556  islaut  40459  ispautN  40475  isldil  40486  isltrn  40495  ltrnid  40511  ltrneq2  40524  isdilN  40530  istrnN  40533  trlval  40538  ltrneq3  40584  cdleme50ex  40935  cdleme  40936  cdlemg1a  40946  ltrniotaval  40957  ltrniotavalbN  40960  cdlemeiota  40961  cdlemg2jlemOLDN  40969  cdlemg2fvlem  40970  cdlemg2klem  40971  istendo  41136  tendoplcbv  41151  tendopl  41152  tendoicbv  41169  tendoi  41170  tendoid0  41201  tendo1ne0  41204  cdlemksv2  41223  cdlemkuv2  41243  cdlemk33N  41285  cdlemk34  41286  cdlemk36  41289  cdlemk19u  41346  cdlemk  41350  tendoex  41351  dvavsca  41393  dvhvscacbv  41474  dvhvscaval  41475  dicopelval  41553  dicelval1sta  41563  diclspsn  41570  dihmeetlem13N  41695  dih1dimatlem0  41704  dih1dimatlem  41705  dihpN  41712  islpolN  41859  hdmap1fval  42172  hdmapfval  42203  sticksstones1  42516  sticksstones2  42517  sticksstones3  42518  sticksstones8  42523  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones12  42528  sticksstones15  42531  frlmsnic  42910  uvcn0  42912  mplmapghm  42922  evlsvarval  42926  evlsbagval  42927  selvvvval  42943  evlselv  42945  fsuppssindlem2  42950  fsuppssind  42951  prjspnfv01  42982  prjspner01  42983  prjspner1  42984  sn-isghm  43031  ismrc  43058  mzpclval  43082  mzpsubst  43105  mzprename  43106  mzpcompact2lem  43108  eldioph  43115  eldioph2  43119  eldioph2b  43120  eldioph3  43123  rexrabdioph  43151  2rexfrabdioph  43153  3rexfrabdioph  43154  4rexfrabdioph  43155  6rexfrabdioph  43156  7rexfrabdioph  43157  eldioph4i  43169  rabren3dioph  43172  mzpcong  43329  jm2.27dlem1  43366  wepwsolem  43399  aomclem6  43416  aomclem8  43418  dfac11  43419  dgraalem  43502  dgraaub  43505  dgraa0p  43506  mpaaeu  43507  mpaalem  43509  aaitgo  43519  rngunsnply  43526  cantnfresb  43681  tfsconcatun  43694  nvocnvb  43778  eliunov2  44035  rfovcnvfvd  44363  fsovfvd  44366  fsovcnvlem  44369  dssmapfv2d  44374  dssmapnvod  44376  clsk1independent  44402  ntrclskb  44425  ntrclsk13  44427  gneispace2  44488  mnringmulrvald  44583  dvconstbi  44690  addrval  44821  subrval  44822  mulvval  44823  relpeq1  45300  fnchoice  45389  refsum2cnlem1  45397  choicefi  45558  axccdom  45580  fmulcl  45941  fmuldfeqlem1  45942  mccllem  45957  mccl  45958  climf  45982  climf2  46024  dvnprodlem1  46304  dvnprodlem3  46306  dvnprod  46307  stoweidlem2  46360  stoweidlem6  46364  stoweidlem8  46366  stoweidlem9  46367  stoweidlem15  46373  stoweidlem16  46374  stoweidlem17  46375  stoweidlem18  46376  stoweidlem21  46379  stoweidlem27  46385  stoweidlem31  46389  stoweidlem36  46394  stoweidlem37  46395  stoweidlem41  46399  stoweidlem43  46401  stoweidlem44  46402  stoweidlem45  46403  stoweidlem46  46404  stoweidlem48  46406  stoweidlem51  46409  stoweidlem55  46413  stoweidlem59  46417  stoweidlem60  46418  stoweidlem62  46420  fourierdlem2  46467  fourierdlem3  46468  elaa2lem  46591  etransclem11  46603  etransclem24  46616  etransclem26  46618  etransclem28  46620  etransclem35  46627  rrndistlt  46648  ioorrnopn  46663  subsaliuncllem  46715  sge0val  46724  ismea  46809  caragenval  46851  isome  46852  isomenndlem  46888  hoicvrrex  46914  ovnlecvr  46916  ovncvrrp  46922  ovn0lem  46923  ovnsubaddlem1  46928  ovnsubadd  46930  hsphoif  46934  hoidmvval  46935  hsphoival  46937  hoidmvlelem3  46955  hoidmvlelem5  46957  hoidmvle  46958  ovnhoilem1  46959  ovnhoi  46961  ovnlecvr2  46968  ovncvr2  46969  hoidifhspval2  46973  hoiqssbllem2  46981  hspmbllem2  46985  hspmbllem3  46986  hspmbl  46987  ovnovollem1  47014  smfmullem2  47150  smfmul  47153  smfpimcclem  47165  chnerlem1  47240  nthrucw  47244  sinnpoly  47251  cfsetsnfsetfv  47417  cfsetsnfsetfo  47420  iccpart  47776  iccpartiun  47794  icceuelpart  47796  nnsum3primes4  48148  nnsum3primesgbe  48152  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  bgoldbtbnd  48169  isisubgr  48222  isgrim  48242  grimidvtxedg  48245  grimcnv  48248  grimco  48249  isuspgrim0  48254  gricushgr  48277  ushggricedg  48287  uhgrimisgrgric  48291  isgrtri  48303  isubgr3stgrlem3  48328  isubgr3stgr  48335  isgrlim  48342  uspgrlim  48352  grlicref  48372  grlicsym  48373  grlictr  48375  grlimedgnedg  48491  isupwlk  48496  lincval  48769  lincdifsn  48784  linindslinci  48808  lindslinindsimp1  48817  linds0  48825  el0ldep  48826  lindsrng01  48828  snlindsntorlem  48830  ldepspr  48833  islindeps2  48843  zlmodzxzldep  48864  bigoval  48909  elbigo  48911  0aryfvalelfv  48995  1arympt1fv  48999  1arymaptfv  49000  1arymaptfo  49003  2arymptfv  49010  2arymaptfv  49011  2arymaptfo  49014  prelrrx2b  49074  rrx2plord  49080  rrx2vlinest  49101  rrx2linesl  49103  elrrx2linest2  49105  line2ylem  49111  line2xlem  49113  itsclc0  49131  itsclc0b  49132  itscnhlinecirc02p  49145  elfvne0  49208  iinfprg  49418  thincciso  49812  thinccisod  49813  setrecseq  50044  aacllem  50160