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 5145	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6545	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6569	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6569	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5143  ℩cio 6512  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569

This theorem is referenced by:  fveq1i  6907  fveq1d  6908  iffv  6923  fvmptd3f  7031  fvmptdv2  7034  eqfnun  7057  fsnex  7303  f1prex  7304  isoeq1  7337  oveq  7437  elovmpt3imp  7690  ofrfvalg  7705  offval  7706  offval3  8007  bropopvvv  8115  bropfvvvvlem  8116  poseq  8183  soseq  8184  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem3OLDa  8351  wfrlem15OLD  8363  smoeq  8390  tfrlem12  8429  tz7.44-2  8447  tz7.44-3  8448  rdgeq1  8451  fsetfocdm  8901  fsetprcnex  8902  mapsncnv  8933  elixp2  8941  resixpfo  8976  elixpsn  8977  mapsnend  9076  enfixsn  9121  mapxpen  9183  ac6sfi  9320  ordtypelem7  9564  wemaplem1  9586  ixpiunwdom  9630  oemapval  9723  cantnf  9733  wemapwe  9737  cnfcom3clem  9745  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  updjud  9974  infxpenc2lem2  10060  fseqenlem1  10064  dfac8clem  10072  ac5num  10076  acni  10085  acni2  10086  acnlem  10088  dfac4  10162  dfac5lem5  10167  dfac2a  10170  dfac9  10177  dfacacn  10182  dfac12lem1  10184  dfac12r  10187  cofsmo  10309  cfsmolem  10310  cfsmo  10311  cfcoflem  10312  coftr  10313  alephsing  10316  isfin3ds  10369  fin23lem17  10378  fin23lem32  10384  fin23lem39  10390  isf33lem  10406  isf34lem6  10420  axcc2lem  10476  axcc3  10478  axdc2lem  10488  axdc3lem2  10491  axdc3lem3  10492  axdc3  10494  axdc4lem  10495  axcclem  10497  ac6num  10519  axdclem2  10560  konigthlem  10608  inar1  10815  1fv  13687  axdc4uzlem  14024  seqeq3  14047  seqof  14100  ccatfval  14611  wrdl1s1  14652  ccat1st1st  14666  cshf1  14848  cshweqrep  14859  wrdlen2i  14981  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  rtrclreclem1  15096  dfrtrclrec2  15097  rtrclreclem2  15098  rtrclreclem4  15100  dfrtrcl2  15101  clim  15530  rlim  15531  ello1  15551  elo1  15562  summo  15753  fsum  15756  prodmo  15972  fprod  15977  bpolylem  16084  bpolyval  16085  vdwlem6  17024  vdwlem8  17026  ramcl  17067  strfvnd  17222  prdsplusgval  17518  prdsmulrval  17520  prdsleval  17522  prdsdsval  17523  prdsvscaval  17524  xpsff1o  17612  isacs2  17696  isnat  17995  yonedalem3b  18324  yonedainv  18326  ismgmhm  18709  ismhm  18798  prdspjmhm  18842  isgrpinv  19011  pwsmulg  19137  isghm  19233  isghmOLD  19234  cayleylem2  19431  symgfix2  19434  gsmsymgrfix  19446  gsmsymgreq  19450  symgfixelq  19451  pmtr3ncomlem2  19492  pmtrdifel  19498  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  psgnunilem2  19513  psgnunilem3  19514  efgsdm  19748  efgredlemd  19762  efgredlem  19765  efgred  19766  efgrelexlema  19767  efgrelexlemb  19768  prdsgsum  19999  pwspjmhmmgpd  20325  pwsexpg  20326  isrnghm  20441  isabv  20812  islmhm  21026  frgpcyg  21592  psgndiflemB  21618  psgndiflemA  21619  dsmmelbas  21759  frlmipval  21799  frlmphl  21801  uvcf1  21812  islindf  21832  islindf4  21858  psrmulfval  21963  evlslem2  22103  evlslem3  22104  evlslem1  22106  mpfrcl  22109  selvval  22139  psdval  22163  psdcoef  22164  psdadd  22167  psdmul  22170  psdmvr  22173  coe1fval  22207  coe1mul2lem2  22271  coe1tm  22276  madetsumid  22467  mvmulval  22549  marepvval0  22572  mulmarep1gsum2  22580  mdetleib2  22594  m1detdiag  22603  mdetralt  22614  mdetunilem7  22624  mdetunilem9  22626  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  symgmatr01lem  22659  gsummatr01lem1  22661  gsummatr01lem4  22664  gsummatr01  22665  smadiadetlem3  22674  pmatcoe1fsupp  22707  pmatcollpw3lem  22789  pmatcollpw3fi1lem2  22793  iscnp  23245  1stcfb  23453  ptpjpre1  23579  elpt  23580  elptr  23581  ptpjopn  23620  dfac14  23626  upxp  23631  pthaus  23646  ptrescn  23647  xkoptsub  23662  cnmptkp  23688  xkofvcn  23692  cnmptk1p  23693  cnmptk2  23694  ptunhmeo  23816  ptcmplem3  24062  ptcmplem4  24063  symgtgp  24114  prdstmdd  24132  isucn  24287  imasdsf1olem  24383  prdsxmslem2  24542  tngngp3  24677  nmoval  24736  elcncf  24915  ishtpy  25004  pcoval  25044  om1elbas  25065  elpi1i  25079  iscau  25310  rrxds  25427  rrxdsfival  25447  ehl1eudisval  25455  ehl2eudisval  25457  mbfi1fseqlem6  25755  mbfi1flimlem  25757  isibl  25800  deg1ldg  26131  deg1leb  26134  elply2  26235  elplyr  26240  ne0p  26246  coeeu  26264  coelem  26265  coeeq  26266  coeidlem  26276  elqaalem3  26363  qaa  26365  iaa  26367  aareccl  26368  aannenlem2  26371  aaliou2  26382  dchrptlem2  27309  dchrpt  27311  dchrsum2  27312  sumdchr2  27314  dchrvmaeq0  27548  rpvmasum2  27556  dchrisum0re  27557  ostth  27683  sltval  27692  nolesgn2o  27716  nogesgn1o  27718  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupfv  27751  noinfcbv  27762  noinffv  27766  iscgrg  28520  isismt  28542  israg  28705  iseqlg  28875  brbtwn  28914  brbtwn2  28920  colinearalg  28925  axsegconlem1  28932  axsegcon  28942  ax5seglem5  28948  axpasch  28956  axlowdim  28976  axeuclidlem  28977  axcontlem1  28979  axcontlem2  28980  axcontlem5  28983  vtxdgfval  29485  1egrvtxdg1  29527  isewlk  29620  iswlk  29628  uspgr2wlkeq2  29665  iswlkon  29675  isclwlk  29793  iscrct  29810  iscycl  29811  iswwlks  29856  wwlknon  29877  wlkiswwlks2  29895  wwlksnredwwlkn0  29916  wlksnwwlknvbij  29928  wwlksnextproplem3  29931  wwlksnextprop  29932  umgr2wlk  29969  midwwlks2s3  29972  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlkslem  29989  rusgrnumwwlkb0  29991  rusgrnumwwlks  29994  isclwwlk  30003  clwlkclwwlklem1  30018  clwwlkn1loopb  30062  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  isclwwlknon  30110  clwwlknon1  30116  s2elclwwlknon2  30123  clwwlkvbij  30132  uhgr3cyclex  30201  fusgreg2wsplem  30352  fusgr2wsp2nb  30353  fusgreghash2wsp  30357  2clwwlkel  30368  extwwlkfabel  30372  numclwwlk1lem2fv  30375  numclwwlk1lem2  30379  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1o  30384  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  ex-fv  30462  isnvlem  30629  islno  30772  nmooval  30782  nmblolbi  30819  isphg  30836  ajmoi  30877  ajval  30880  ubthlem3  30891  htthlem  30936  hcau  31203  hlimi  31207  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  adjmo  31851  nmopval  31875  elcnop  31876  ellnop  31877  elunop  31891  elhmop  31892  nmfnval  31895  elcnfn  31901  ellnfn  31902  adjeu  31908  adjval  31909  eigvecval  31915  eigvalfval  31916  adj1  31952  adjeq  31954  hmopadj2  31960  lnopeq0i  32026  lnopeq  32028  elunop2  32032  lnophm  32038  hmopco  32042  nmbdoplb  32044  nmcoplb  32049  lnopcon  32054  lnfn0  32066  lnfnmul  32067  nmbdfnlb  32069  nmcfnlb  32073  lnfncon  32075  riesz4  32083  riesz1  32084  cnlnadjlem9  32094  cnlnadjeu  32097  cnlnssadj  32099  nmopcoi  32114  bra11  32127  cnvbraval  32129  pjss2coi  32183  pjssdif2i  32193  pjssdif1i  32194  pjclem4  32218  pj3si  32226  pj3cor1i  32228  isst  32232  ishst  32233  stri  32276  hstri  32284  aciunf1lem  32672  ismnt  32973  mgcval  32977  ischn  32996  chnind  33001  chnub  33002  fzo0pmtrlast  33112  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspn  33250  elrgspnsubrunlem1  33251  linds2eq  33409  elrspunidl  33456  elrspunsn  33457  dfufd2lem  33577  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  fldextrspunlsplem  33723  fldextrspunlsp  33724  fldext2chn  33769  constrextdg2lem  33789  constrextdg2  33790  lmatval  33812  mdetpmtr1  33822  zarcmplem  33880  ismeas  34200  isrnmeas  34201  cntnevol  34229  carsgval  34305  sitgval  34334  eulerpartleme  34365  eulerpartlemd  34368  eulerpartlemr  34376  eulerpartlemgvv  34378  eulerpart  34384  cndprobval  34435  signstfvneq0  34587  reprsum  34628  reprsuc  34630  reprpmtf1o  34641  reprdifc  34642  breprexp  34648  vtsval  34652  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  bnj66  34874  bnj106  34882  bnj125  34886  bnj154  34892  bnj155  34893  bnj526  34902  bnj540  34906  bnj609  34931  bnj611  34932  bnj893  34942  bnj1000  34955  bnj1014  34975  bnj1015  34976  bnj1234  35027  bnj1463  35069  gblacfnacd  35113  loop1cycl  35142  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  subfacp1  35191  sconnpht  35234  cnpconn  35235  txpconn  35237  ptpconn  35238  indispconn  35239  connpconn  35240  cvxpconn  35247  cvmliftmo  35289  cvmliftlem14  35302  cvmliftlem15  35303  cvmliftiota  35306  cvmlift2  35321  cvmliftphtlem  35322  cvmlift3lem2  35325  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  cvmlift3  35333  satfv1lem  35367  satfv1  35368  sategoelfvb  35424  mrsubff1  35519  mrsub0  35521  mrsubccat  35523  mrsubcn  35524  elmsubrn  35533  msubrn  35534  msubco  35536  msubvrs  35565  mclsax  35574  shftvalg  35732  fwddifval  36163  fwddifnval  36164  bj-evalval  37076  unceq  37604  matunitlindflem2  37624  poimirlem17  37644  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem27  37654  poimirlem28  37655  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  poimir  37660  broucube  37661  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anclem2  37701  ftc1anclem5  37704  upixp  37736  fdc  37752  isismty  37808  rrnmval  37835  elghomlem2OLD  37893  isrngohom  37972  islfl  39061  isopos  39181  islaut  40085  ispautN  40101  isldil  40112  isltrn  40121  ltrnid  40137  ltrneq2  40150  isdilN  40156  istrnN  40159  trlval  40164  ltrneq3  40210  cdleme50ex  40561  cdleme  40562  cdlemg1a  40572  ltrniotaval  40583  ltrniotavalbN  40586  cdlemeiota  40587  cdlemg2jlemOLDN  40595  cdlemg2fvlem  40596  cdlemg2klem  40597  istendo  40762  tendoplcbv  40777  tendopl  40778  tendoicbv  40795  tendoi  40796  tendoid0  40827  tendo1ne0  40830  cdlemksv2  40849  cdlemkuv2  40869  cdlemk33N  40911  cdlemk34  40912  cdlemk36  40915  cdlemk19u  40972  cdlemk  40976  tendoex  40977  dvavsca  41019  dvhvscacbv  41100  dvhvscaval  41101  dicopelval  41179  dicelval1sta  41189  diclspsn  41196  dihmeetlem13N  41321  dih1dimatlem0  41330  dih1dimatlem  41331  dihpN  41338  islpolN  41485  hdmap1fval  41798  hdmapfval  41829  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones8  42154  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones15  42162  frlmsnic  42550  uvcn0  42552  pwsgprod  42554  mplmapghm  42566  evlsvval  42570  evlsvvval  42573  evlsvarval  42575  evlsbagval  42576  selvvvval  42595  evlselv  42597  fsuppssindlem2  42602  fsuppssind  42603  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  sn-isghm  42683  ismrc  42712  mzpclval  42736  mzpsubst  42759  mzprename  42760  mzpcompact2lem  42762  eldioph  42769  eldioph2  42773  eldioph2b  42774  eldioph3  42777  rexrabdioph  42805  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  eldioph4i  42823  rabren3dioph  42826  mzpcong  42984  jm2.27dlem1  43021  wepwsolem  43054  aomclem6  43071  aomclem8  43073  dfac11  43074  dgraalem  43157  dgraaub  43160  dgraa0p  43161  mpaaeu  43162  mpaalem  43164  aaitgo  43174  rngunsnply  43181  cantnfresb  43337  tfsconcatun  43350  nvocnvb  43435  eliunov2  43692  rfovcnvfvd  44020  fsovfvd  44023  fsovcnvlem  44026  dssmapfv2d  44031  dssmapnvod  44033  clsk1independent  44059  ntrclskb  44082  ntrclsk13  44084  gneispace2  44145  mnringmulrvald  44246  dvconstbi  44353  addrval  44485  subrval  44486  mulvval  44487  relpeq1  44965  fnchoice  45034  refsum2cnlem1  45042  choicefi  45205  axccdom  45227  fmulcl  45596  fmuldfeqlem1  45597  mccllem  45612  mccl  45613  climf  45637  climf2  45681  dvnprodlem1  45961  dvnprodlem3  45963  dvnprod  45964  stoweidlem2  46017  stoweidlem6  46021  stoweidlem8  46023  stoweidlem9  46024  stoweidlem15  46030  stoweidlem16  46031  stoweidlem17  46032  stoweidlem18  46033  stoweidlem21  46036  stoweidlem27  46042  stoweidlem31  46046  stoweidlem36  46051  stoweidlem37  46052  stoweidlem41  46056  stoweidlem43  46058  stoweidlem44  46059  stoweidlem45  46060  stoweidlem46  46061  stoweidlem48  46063  stoweidlem51  46066  stoweidlem55  46070  stoweidlem59  46074  stoweidlem60  46075  stoweidlem62  46077  fourierdlem2  46124  fourierdlem3  46125  elaa2lem  46248  etransclem11  46260  etransclem24  46273  etransclem26  46275  etransclem28  46277  etransclem35  46284  rrndistlt  46305  ioorrnopn  46320  subsaliuncllem  46372  sge0val  46381  ismea  46466  caragenval  46508  isome  46509  isomenndlem  46545  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  ovnsubadd  46587  hsphoif  46591  hoidmvval  46592  hsphoival  46594  hoidmvlelem3  46612  hoidmvlelem5  46614  hoidmvle  46615  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  ovncvr2  46626  hoidifhspval2  46630  hoiqssbllem2  46638  hspmbllem2  46642  hspmbllem3  46643  hspmbl  46644  ovnovollem1  46671  smfmullem2  46807  smfmul  46810  smfpimcclem  46822  tworepnotupword  46901  cfsetsnfsetfv  47069  cfsetsnfsetfo  47072  iccpart  47403  iccpartiun  47421  icceuelpart  47423  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbnd  47796  isisubgr  47848  isgrim  47868  isuspgrim0  47872  grimidvtxedg  47876  grimcnv  47879  grimco  47880  gricushgr  47886  ushggricedg  47896  uhgrimisgrgric  47899  isgrtri  47910  isubgr3stgrlem3  47935  isubgr3stgr  47942  isgrlim  47949  uspgrlim  47959  grlicref  47972  grlicsym  47973  grlictr  47975  isupwlk  48052  lincval  48326  lincdifsn  48341  linindslinci  48365  lindslinindsimp1  48374  linds0  48382  el0ldep  48383  lindsrng01  48385  snlindsntorlem  48387  ldepspr  48390  islindeps2  48400  zlmodzxzldep  48421  bigoval  48470  elbigo  48472  0aryfvalelfv  48556  1arympt1fv  48560  1arymaptfv  48561  1arymaptfo  48564  2arymptfv  48571  2arymaptfv  48572  2arymaptfo  48575  prelrrx2b  48635  rrx2plord  48641  rrx2vlinest  48662  rrx2linesl  48664  elrrx2linest2  48666  line2ylem  48672  line2xlem  48674  itsclc0  48692  itsclc0b  48693  itscnhlinecirc02p  48706  elfvne0  48758  thincciso  49102  thinccisod  49103  setrecseq  49204  aacllem  49320