Theorem fveq1 6905

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 5149	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6546	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6570	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6570	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147  ℩cio 6513  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570

This theorem is referenced by:  fveq1i  6907  fveq1d  6908  iffv  6923  fvmptd3f  7030  fvmptdv2  7033  eqfnun  7056  fsnex  7302  f1prex  7303  isoeq1  7336  oveq  7436  elovmpt3imp  7689  ofrfvalg  7704  offval  7705  offval3  8005  bropopvvv  8113  bropfvvvvlem  8114  poseq  8181  soseq  8182  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem3OLDa  8349  wfrlem15OLD  8361  smoeq  8388  tfrlem12  8427  tz7.44-2  8445  tz7.44-3  8446  rdgeq1  8449  fsetfocdm  8899  fsetprcnex  8900  mapsncnv  8931  elixp2  8939  resixpfo  8974  elixpsn  8975  mapsnend  9074  enfixsn  9119  mapxpen  9181  ac6sfi  9317  ordtypelem7  9561  wemaplem1  9583  ixpiunwdom  9627  oemapval  9720  cantnf  9730  wemapwe  9734  cnfcom3clem  9742  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  updjud  9971  infxpenc2lem2  10057  fseqenlem1  10061  dfac8clem  10069  ac5num  10073  acni  10082  acni2  10083  acnlem  10085  dfac4  10159  dfac5lem5  10164  dfac2a  10167  dfac9  10174  dfacacn  10179  dfac12lem1  10181  dfac12r  10184  cofsmo  10306  cfsmolem  10307  cfsmo  10308  cfcoflem  10309  coftr  10310  alephsing  10313  isfin3ds  10366  fin23lem17  10375  fin23lem32  10381  fin23lem39  10387  isf33lem  10403  isf34lem6  10417  axcc2lem  10473  axcc3  10475  axdc2lem  10485  axdc3lem2  10488  axdc3lem3  10489  axdc3  10491  axdc4lem  10492  axcclem  10494  ac6num  10516  axdclem2  10557  konigthlem  10605  inar1  10812  1fv  13683  axdc4uzlem  14020  seqeq3  14043  seqof  14096  ccatfval  14607  wrdl1s1  14648  ccat1st1st  14662  cshf1  14844  cshweqrep  14855  wrdlen2i  14977  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  wrd2f1tovbij  14995  rtrclreclem1  15092  dfrtrclrec2  15093  rtrclreclem2  15094  rtrclreclem4  15096  dfrtrcl2  15097  clim  15526  rlim  15527  ello1  15547  elo1  15558  summo  15749  fsum  15752  prodmo  15968  fprod  15973  bpolylem  16080  bpolyval  16081  vdwlem6  17019  vdwlem8  17021  ramcl  17062  strfvnd  17218  prdsplusgval  17519  prdsmulrval  17521  prdsleval  17523  prdsdsval  17524  prdsvscaval  17525  xpsff1o  17613  isacs2  17697  isnat  18001  yonedalem3b  18335  yonedainv  18337  ismgmhm  18721  ismhm  18810  prdspjmhm  18854  isgrpinv  19023  pwsmulg  19149  isghm  19245  isghmOLD  19246  cayleylem2  19445  symgfix2  19448  gsmsymgrfix  19460  gsmsymgreq  19464  symgfixelq  19465  pmtr3ncomlem2  19506  pmtrdifel  19512  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  psgnunilem2  19527  psgnunilem3  19528  efgsdm  19762  efgredlemd  19776  efgredlem  19779  efgred  19780  efgrelexlema  19781  efgrelexlemb  19782  prdsgsum  20013  pwspjmhmmgpd  20341  pwsexpg  20342  isrnghm  20457  isabv  20828  islmhm  21043  frgpcyg  21609  psgndiflemB  21635  psgndiflemA  21636  dsmmelbas  21776  frlmipval  21816  frlmphl  21818  uvcf1  21829  islindf  21849  islindf4  21875  psrmulfval  21980  evlslem2  22120  evlslem3  22121  evlslem1  22123  mpfrcl  22126  selvval  22156  psdval  22180  psdcoef  22181  psdadd  22184  psdmul  22187  coe1fval  22222  coe1mul2lem2  22286  coe1tm  22291  madetsumid  22482  mvmulval  22564  marepvval0  22587  mulmarep1gsum2  22595  mdetleib2  22609  m1detdiag  22618  mdetralt  22629  mdetunilem7  22639  mdetunilem9  22641  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  symgmatr01lem  22674  gsummatr01lem1  22676  gsummatr01lem4  22679  gsummatr01  22680  smadiadetlem3  22689  pmatcoe1fsupp  22722  pmatcollpw3lem  22804  pmatcollpw3fi1lem2  22808  iscnp  23260  1stcfb  23468  ptpjpre1  23594  elpt  23595  elptr  23596  ptpjopn  23635  dfac14  23641  upxp  23646  pthaus  23661  ptrescn  23662  xkoptsub  23677  cnmptkp  23703  xkofvcn  23707  cnmptk1p  23708  cnmptk2  23709  ptunhmeo  23831  ptcmplem3  24077  ptcmplem4  24078  symgtgp  24129  prdstmdd  24147  isucn  24302  imasdsf1olem  24398  prdsxmslem2  24557  tngngp3  24692  nmoval  24751  elcncf  24928  ishtpy  25017  pcoval  25057  om1elbas  25078  elpi1i  25092  iscau  25323  rrxds  25440  rrxdsfival  25460  ehl1eudisval  25468  ehl2eudisval  25470  mbfi1fseqlem6  25769  mbfi1flimlem  25771  isibl  25814  deg1ldg  26145  deg1leb  26148  elply2  26249  elplyr  26254  ne0p  26260  coeeu  26278  coelem  26279  coeeq  26280  coeidlem  26290  elqaalem3  26377  qaa  26379  iaa  26381  aareccl  26382  aannenlem2  26385  aaliou2  26396  dchrptlem2  27323  dchrpt  27325  dchrsum2  27326  sumdchr2  27328  dchrvmaeq0  27562  rpvmasum2  27570  dchrisum0re  27571  ostth  27697  sltval  27706  nolesgn2o  27730  nogesgn1o  27732  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupfv  27765  noinfcbv  27776  noinffv  27780  iscgrg  28534  isismt  28556  israg  28719  iseqlg  28889  brbtwn  28928  brbtwn2  28934  colinearalg  28939  axsegconlem1  28946  axsegcon  28956  ax5seglem5  28962  axpasch  28970  axlowdim  28990  axeuclidlem  28991  axcontlem1  28993  axcontlem2  28994  axcontlem5  28997  vtxdgfval  29499  1egrvtxdg1  29541  isewlk  29634  iswlk  29642  uspgr2wlkeq2  29679  iswlkon  29689  isclwlk  29805  iscrct  29822  iscycl  29823  iswwlks  29865  wwlknon  29886  wlkiswwlks2  29904  wwlksnredwwlkn0  29925  wlksnwwlknvbij  29937  wwlksnextproplem3  29940  wwlksnextprop  29941  umgr2wlk  29978  midwwlks2s3  29981  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlkslem  29998  rusgrnumwwlkb0  30000  rusgrnumwwlks  30003  isclwwlk  30012  clwlkclwwlklem1  30027  clwwlkn1loopb  30071  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  isclwwlknon  30119  clwwlknon1  30125  s2elclwwlknon2  30132  clwwlkvbij  30141  uhgr3cyclex  30210  fusgreg2wsplem  30361  fusgr2wsp2nb  30362  fusgreghash2wsp  30366  2clwwlkel  30377  extwwlkfabel  30381  numclwwlk1lem2fv  30384  numclwwlk1lem2  30388  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1o  30393  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  ex-fv  30471  isnvlem  30638  islno  30781  nmooval  30791  nmblolbi  30828  isphg  30845  ajmoi  30886  ajval  30889  ubthlem3  30900  htthlem  30945  hcau  31212  hlimi  31216  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  adjmo  31860  nmopval  31884  elcnop  31885  ellnop  31886  elunop  31900  elhmop  31901  nmfnval  31904  elcnfn  31910  ellnfn  31911  adjeu  31917  adjval  31918  eigvecval  31924  eigvalfval  31925  adj1  31961  adjeq  31963  hmopadj2  31969  lnopeq0i  32035  lnopeq  32037  elunop2  32041  lnophm  32047  hmopco  32051  nmbdoplb  32053  nmcoplb  32058  lnopcon  32063  lnfn0  32075  lnfnmul  32076  nmbdfnlb  32078  nmcfnlb  32082  lnfncon  32084  riesz4  32092  riesz1  32093  cnlnadjlem9  32103  cnlnadjeu  32106  cnlnssadj  32108  nmopcoi  32123  bra11  32136  cnvbraval  32138  pjss2coi  32192  pjssdif2i  32202  pjssdif1i  32203  pjclem4  32227  pj3si  32235  pj3cor1i  32237  isst  32241  ishst  32242  stri  32285  hstri  32293  aciunf1lem  32678  ismnt  32957  mgcval  32961  ischn  32980  chnind  32984  chnub  32985  fzo0pmtrlast  33094  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  elrgspn  33235  linds2eq  33388  elrspunidl  33435  elrspunsn  33436  dfufd2lem  33556  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  fldext2chn  33733  lmatval  33773  mdetpmtr1  33783  zarcmplem  33841  ismeas  34179  isrnmeas  34180  cntnevol  34208  carsgval  34284  sitgval  34313  eulerpartleme  34344  eulerpartlemd  34347  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpart  34363  cndprobval  34414  signstfvneq0  34565  reprsum  34606  reprsuc  34608  reprpmtf1o  34619  reprdifc  34620  breprexp  34626  vtsval  34630  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  bnj66  34852  bnj106  34860  bnj125  34864  bnj154  34870  bnj155  34871  bnj526  34880  bnj540  34884  bnj609  34909  bnj611  34910  bnj893  34920  bnj1000  34933  bnj1014  34953  bnj1015  34954  bnj1234  35005  bnj1463  35047  gblacfnacd  35091  loop1cycl  35121  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  subfacp1  35170  sconnpht  35213  cnpconn  35214  txpconn  35216  ptpconn  35217  indispconn  35218  connpconn  35219  cvxpconn  35226  cvmliftmo  35268  cvmliftlem14  35281  cvmliftlem15  35282  cvmliftiota  35285  cvmlift2  35300  cvmliftphtlem  35301  cvmlift3lem2  35304  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  cvmlift3  35312  satfv1lem  35346  satfv1  35347  sategoelfvb  35403  mrsubff1  35498  mrsub0  35500  mrsubccat  35502  mrsubcn  35503  elmsubrn  35512  msubrn  35513  msubco  35515  msubvrs  35544  mclsax  35553  shftvalg  35711  fwddifval  36143  fwddifnval  36144  bj-evalval  37057  unceq  37583  matunitlindflem2  37603  poimirlem17  37623  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem27  37633  poimirlem28  37634  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  poimir  37639  broucube  37640  voliunnfl  37650  volsupnfl  37651  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  ftc1anclem2  37680  ftc1anclem5  37683  upixp  37715  fdc  37731  isismty  37787  rrnmval  37814  elghomlem2OLD  37872  isrngohom  37951  islfl  39041  isopos  39161  islaut  40065  ispautN  40081  isldil  40092  isltrn  40101  ltrnid  40117  ltrneq2  40130  isdilN  40136  istrnN  40139  trlval  40144  ltrneq3  40190  cdleme50ex  40541  cdleme  40542  cdlemg1a  40552  ltrniotaval  40563  ltrniotavalbN  40566  cdlemeiota  40567  cdlemg2jlemOLDN  40575  cdlemg2fvlem  40576  cdlemg2klem  40577  istendo  40742  tendoplcbv  40757  tendopl  40758  tendoicbv  40775  tendoi  40776  tendoid0  40807  tendo1ne0  40810  cdlemksv2  40829  cdlemkuv2  40849  cdlemk33N  40891  cdlemk34  40892  cdlemk36  40895  cdlemk19u  40952  cdlemk  40956  tendoex  40957  dvavsca  40999  dvhvscacbv  41080  dvhvscaval  41081  dicopelval  41159  dicelval1sta  41169  diclspsn  41176  dihmeetlem13N  41301  dih1dimatlem0  41310  dih1dimatlem  41311  dihpN  41318  islpolN  41465  hdmap1fval  41778  hdmapfval  41809  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones15  42142  frlmsnic  42526  uvcn0  42528  pwsgprod  42530  mplmapghm  42542  evlsvval  42546  evlsvvval  42549  evlsvarval  42551  evlsbagval  42552  selvvvval  42571  evlselv  42573  fsuppssindlem2  42578  fsuppssind  42579  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  sn-isghm  42659  ismrc  42688  mzpclval  42712  mzpsubst  42735  mzprename  42736  mzpcompact2lem  42738  eldioph  42745  eldioph2  42749  eldioph2b  42750  eldioph3  42753  rexrabdioph  42781  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  eldioph4i  42799  rabren3dioph  42802  mzpcong  42960  jm2.27dlem1  42997  wepwsolem  43030  aomclem6  43047  aomclem8  43049  dfac11  43050  dgraalem  43133  dgraaub  43136  dgraa0p  43137  mpaaeu  43138  mpaalem  43140  aaitgo  43150  rngunsnply  43157  cantnfresb  43313  tfsconcatun  43326  nvocnvb  43411  eliunov2  43668  rfovcnvfvd  43996  fsovfvd  43999  fsovcnvlem  44002  dssmapfv2d  44007  dssmapnvod  44009  clsk1independent  44035  ntrclskb  44058  ntrclsk13  44060  gneispace2  44121  mnringmulrvald  44222  dvconstbi  44329  addrval  44461  subrval  44462  mulvval  44463  fnchoice  44966  refsum2cnlem1  44974  choicefi  45142  axccdom  45164  fmulcl  45536  fmuldfeqlem1  45537  mccllem  45552  mccl  45553  climf  45577  climf2  45621  dvnprodlem1  45901  dvnprodlem3  45903  dvnprod  45904  stoweidlem2  45957  stoweidlem6  45961  stoweidlem8  45963  stoweidlem9  45964  stoweidlem15  45970  stoweidlem16  45971  stoweidlem17  45972  stoweidlem18  45973  stoweidlem21  45976  stoweidlem27  45982  stoweidlem31  45986  stoweidlem36  45991  stoweidlem37  45992  stoweidlem41  45996  stoweidlem43  45998  stoweidlem44  45999  stoweidlem45  46000  stoweidlem46  46001  stoweidlem48  46003  stoweidlem51  46006  stoweidlem55  46010  stoweidlem59  46014  stoweidlem60  46015  stoweidlem62  46017  fourierdlem2  46064  fourierdlem3  46065  elaa2lem  46188  etransclem11  46200  etransclem24  46213  etransclem26  46215  etransclem28  46217  etransclem35  46224  rrndistlt  46245  ioorrnopn  46260  subsaliuncllem  46312  sge0val  46321  ismea  46406  caragenval  46448  isome  46449  isomenndlem  46485  hoicvrrex  46511  ovnlecvr  46513  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  ovnsubadd  46527  hsphoif  46531  hoidmvval  46532  hsphoival  46534  hoidmvlelem3  46552  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem1  46556  ovnhoi  46558  ovnlecvr2  46565  ovncvr2  46566  hoidifhspval2  46570  hoiqssbllem2  46578  hspmbllem2  46582  hspmbllem3  46583  hspmbl  46584  ovnovollem1  46611  smfmullem2  46747  smfmul  46750  smfpimcclem  46762  tworepnotupword  46839  cfsetsnfsetfv  47006  cfsetsnfsetfo  47009  iccpart  47340  iccpartiun  47358  icceuelpart  47360  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbnd  47733  isisubgr  47785  isgrim  47805  isuspgrim0  47809  grimidvtxedg  47813  grimcnv  47816  grimco  47817  gricushgr  47823  ushggricedg  47833  uhgrimisgrgric  47836  isgrtri  47847  isubgr3stgrlem3  47870  isubgr3stgr  47877  isgrlim  47884  uspgrlim  47894  grlicref  47907  grlicsym  47908  grlictr  47910  isupwlk  47979  lincval  48254  lincdifsn  48269  linindslinci  48293  lindslinindsimp1  48302  linds0  48310  el0ldep  48311  lindsrng01  48313  snlindsntorlem  48315  ldepspr  48318  islindeps2  48328  zlmodzxzldep  48349  bigoval  48398  elbigo  48400  0aryfvalelfv  48484  1arympt1fv  48488  1arymaptfv  48489  1arymaptfo  48492  2arymptfv  48499  2arymaptfv  48500  2arymaptfo  48503  prelrrx2b  48563  rrx2plord  48569  rrx2vlinest  48590  rrx2linesl  48592  elrrx2linest2  48594  line2ylem  48600  line2xlem  48602  itsclc0  48620  itsclc0b  48621  itscnhlinecirc02p  48634  elfvne0  48678  thincciso  48848  thinccisod  48849  setrecseq  48915  aacllem  49031