Theorem fveq2i 6106

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fveq2i	⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fveq2 6103	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1475  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812

This theorem is referenced by:  fveq12i  6108  ot1stg  7073  ot2ndg  7074  ot3rdg  7075  algrflem  7173  wfrlem5  7306  wfrlem14  7315  tfr2a  7378  rdgsucmptf  7411  rdgsucmptnf  7412  frsucmpt  7420  frsucmptn  7421  infiso  8296  inf3lemc  8406  cantnf  8473  wemapwe  8477  cnfcom2lem  8481  cnfcom2  8482  cnfcom3lem  8483  r1sucg  8515  rankprb  8597  rankopb  8598  ranksuc  8611  rankmapu  8624  cardiun  8691  alephsuc  8774  alephcard  8776  alephfplem2  8811  ackbij1lem8  8932  ackbij1lem13  8937  ackbij1lem14  8938  ackbij2lem2  8945  infpssrlem2  9009  fin23lem34  9051  fin23lem35  9052  aleph1  9272  pwcfsdom  9284  cfpwsdom  9285  alephom  9286  rankcf  9478  addpqnq  9639  mulpqnq  9642  addcomnq  9652  mulcomnq  9654  addclprlem2  9718  infrenegsup  10883  fseq1p1m1  12283  fz0to4untppr  12311  fldiv4p1lem1div2  12498  om2uzrdg  12617  uzrdgsuci  12621  fzennn  12629  axdc4uzlem  12644  seqp1i  12679  seqf1olem2  12703  facp1  12927  fac2  12928  fac3  12929  fac4  12930  4bc2eq6  12978  hashcard  13008  hasheq0  13015  hashun2  13033  hashun3  13034  hashprg  13043  hashprgOLD  13044  hashprb  13046  hashprdifel  13047  hashp1i  13052  pr0hash2ex  13057  hashdif  13062  hashunlei  13072  hashfzo  13076  hashxplem  13080  hashmap  13082  hashfun  13084  hashimarn  13085  hashbclem  13093  hashbc  13094  hashf1lem2  13097  hashtpg  13121  ccatalpha  13228  s1len  13238  revs1  13365  cats1len  13456  lsws2  13499  lsws3  13500  lsws4  13501  rei  13744  imi  13745  sqrt1  13860  sqrt4  13861  sqrt9  13862  abs0  13873  absi  13874  sqreulem  13947  fsumabs  14374  fsumrelem  14380  o1fsum  14386  hashrabrex  14396  hashuni  14397  incexclem  14407  incexc  14408  isumnn0nn  14413  fprodefsum  14664  efsep  14679  sin0  14718  cos0  14719  ef01bndlem  14753  cos2bnd  14757  sin4lt0  14764  ruclem6  14803  aleph1re  14813  pwp1fsum  14952  m1bits  15000  sadcaddlem  15017  sadaddlem  15026  sadeq  15032  algrp1  15125  eucalg  15138  prmind2  15236  dfphi2  15317  phiprmpw  15319  phimullem  15322  pockthlem  15447  pockthg  15448  prmunb  15456  prmreclem4  15461  vdwap1  15519  vdwlem12  15534  prmo2  15582  prmo3  15583  prmgaplem7  15599  prmo4  15673  prmo5  15674  prmo6  15675  ndxid  15716  dfpleOLD  15789  imasvsca  16003  mreexdomd  16133  isoval  16248  yonedalem21  16736  yonedalem22  16741  joincomALT  16852  meetcomALT  16854  lubsn  16917  oduleval  16954  odubas  16956  isacs5lem  16992  acsmapd  17001  oppgplusfval  17601  oppglem  17603  symghash  17628  symg1hash  17638  symg2hash  17640  symggen  17713  psgnsn  17763  psgnprfval1  17765  psgnprfval2  17766  odngen  17815  sylow1lem1  17836  efgs1b  17972  efgsfo  17975  efgredlemg  17978  efgredlemd  17980  frgpuplem  18008  gsumzmhm  18160  gsumzinv  18168  dprd2da  18264  dmdprdsplit2lem  18267  pgpfaclem1  18303  mgpplusg  18316  mgplem  18317  ringidval  18326  opprmulfval  18448  opprlem  18451  isrhm2d  18551  rhm1  18553  lspprid2  18819  lsmpr  18910  lsppr  18914  lspsntri  18918  lbspropd  18920  lspexchn2  18952  lspindp2l  18955  lspindp2  18956  lspsnat  18966  lsppratlem1  18968  lsppratlem3  18970  lsppratlem4  18971  lidlrsppropd  19051  asclfval  19155  assamulgscmlem2  19170  evlsval  19340  psropprmul  19429  ply1sca2  19445  ply1mpl0  19446  ply1mpl1  19448  coe1fzgsumd  19493  evls1var  19523  evl1gsumd  19542  evl1varpw  19546  evl1varpwval  19547  evl1scvarpw  19548  zrhpsgnodpm  19757  psgnfix1  19763  psgnfix2  19764  psgndiflemB  19765  dsmmbas2  19900  dsmmelbas  19902  dsmmsubg  19906  frlmip  19936  islinds2  19971  lindsind2  19977  lindfmm  19985  islindf4  19996  mat1bas  20074  mat0dim0  20092  mat0dimid  20093  mat0dimscm  20094  mat0dimcrng  20095  mat1rhmelval  20105  dmatval  20117  scmatval  20129  mat1scmat  20164  1mavmul  20173  marrepfval  20185  marepvfval  20190  ma1repvcl  20195  ma1repveval  20196  submafval  20204  mdetfval1  20215  mdetralt  20233  mdetunilem7  20243  m2detleiblem3  20254  m2detleiblem4  20255  madufval  20262  maducoeval2  20265  madugsum  20268  minmar1fval  20271  cramerimplem1  20308  cramer0  20315  pmatcoe1fsupp  20325  cpmat  20333  mat2pmatfval  20347  mat2pmatmul  20355  idmatidpmat  20361  m2cpminv0  20385  pmatcollpwfi  20406  pmatcollpw3fi1lem1  20410  pm2mpval  20419  chpmatval2  20457  cpmidpmat  20497  cayleyhamilton1  20516  sn0cld  20704  lpdifsn  20757  restcls  20795  restntr  20796  ordtrest2  20818  leordtval  20827  pttoponconst  21210  ptclsg  21228  xkoptsub  21267  xkofvcn  21297  tgqtop  21325  hmeocls  21381  hmeontr  21382  ptcmpfi  21426  ptcmplem1  21666  tmdgsum  21709  utop2nei  21864  cuspcvg  21915  iscusp2  21916  cnextucn  21917  comet  22128  nrmmetd  22189  isngp3  22212  ngpds  22218  tngnm  22265  cnmetdval  22384  qdensere2  22408  tgioo3  22416  cnmpt2pc  22535  cnheibor  22562  htpyco2  22586  phtpyco2  22597  pco0  22622  pi1xfrcnv  22665  cnrbas  22750  cncvs  22753  cnnm  22768  ipcau2  22841  cfilfcls  22880  cncmet  22927  reust  22977  rrxprds  22985  pjthlem1  23016  ovolunlem1a  23071  ovolfiniun  23076  ovoliunlem2  23078  ovoliunlem3  23079  ovoliun  23080  ovolicc1  23091  ismbl2  23102  unmbl  23112  volinun  23121  volfiniun  23122  voliunlem1  23125  voliunlem2  23126  ioorinv  23150  mbfimaopnlem  23228  itg2cnlem2  23335  itg2cn  23336  dfitg  23342  itg0  23352  iblre  23366  itgreval  23369  itgitg2  23379  iblconst  23390  itgconst  23391  itgcn  23415  limcflflem  23450  dvn1  23495  dvlipcn  23561  c1lip2  23565  dvcnvrelem2  23585  ply1divalg2  23702  ply1remlem  23726  dgr0  23822  elqaalem2  23879  dvradcnv  23979  pserdvlem2  23986  pserdv2  23988  abelthlem6  23994  abelthlem9  23998  sinhalfpilem  24019  cospi  24028  sincos4thpi  24069  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  sinkpi  24075  eflog  24127  logfac  24151  logdmopn  24195  logtayl  24206  cxpcn3  24289  root1eq1  24296  cxpeq  24298  logbleb  24321  logblt  24322  ang180lem1  24339  ang180lem2  24340  ang180lem4  24342  lawcos  24346  1cubrlem  24368  asin1  24421  atan0  24435  atan1  24455  log2cnv  24471  birthdaylem2  24479  lgamgulmlem2  24556  gam1  24591  ftalem3  24601  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  ppi1  24690  ppi1i  24694  ppi2i  24695  cht2  24698  cht3  24699  ppiub  24729  chtub  24737  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgsval2lem  24832  lgsqrlem1  24871  lgsqrlem4  24874  lgsquadlem2  24906  chebbnd1  24961  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0flb  24999  mulog2sumlem2  25024  pntpbnd1a  25074  pntlemf  25094  cchhllem  25567  axlowdimlem17  25638  graop  25706  uhgrstrrepe  25745  usgraexmplcvtx  25934  usgraexmplcedg  25935  wlkntrllem2  26090  2pthon  26132  usgra2adedgwlkon  26143  constr3cycllem1  26186  wlknwwlknsur  26240  wlkiswwlksur  26247  0clwlk  26293  clwwlkgt0  26299  clwlkfclwwlk1hashn  26368  clwlkfoclwwlk  26372  vdgr0  26427  clwlknclwlkdifnum  26488  eupap1  26503  eupath2lem3  26506  numclwwlkovf2num  26612  ex-co  26687  ex-ceil  26697  ex-fac  26700  ex-hash  26702  ex-sqrt  26703  ex-prmo  26708  0vfval  26845  nvvop  26848  vsfval  26872  cnnvg  26917  cnnvs  26919  cnnvnm  26920  imsdval  26925  ipidsq  26949  nmblolbii  27038  blocnilem  27043  ip0i  27064  ip1ilem  27065  ipasslem10  27078  siilem1  27090  cnbn  27109  h2hva  27215  h2hsm  27216  h2hnm  27217  axhfvadd-zf  27223  axhvcom-zf  27224  axhvass-zf  27225  axhv0cl-zf  27226  axhvaddid-zf  27227  axhfvmul-zf  27228  axhvmulid-zf  27229  axhvmulass-zf  27230  axhvdistr1-zf  27231  axhvdistr2-zf  27232  axhvmul0-zf  27233  axhfi-zf  27234  axhis1-zf  27235  axhis2-zf  27236  axhis3-zf  27237  axhis4-zf  27238  axhcompl-zf  27239  norm-iii-i  27380  normsubi  27382  norm3difi  27388  normpar2i  27397  hh0v  27409  hhssva  27498  hhsssm  27499  hhssnm  27500  hhshsslem1  27508  hhsscms  27520  choc1  27570  shjcom  27601  pjhthlem1  27634  pjoc2i  27681  shs0i  27692  chj0i  27698  chdmj1i  27724  chjassi  27729  spansn0  27784  spanpr  27823  qlaxr4i  27877  pjadjii  27917  pjaddii  27918  pjmulii  27920  pjsubii  27921  pjcji  27927  pjnormi  27964  pjpythi  27965  ho0val  27993  lnop0  28209  lnophmlem2  28260  nmbdoplbi  28267  nmcopexi  28270  lnfn0i  28285  nmcfnexi  28294  nmopadji  28333  nmoptri2i  28342  nmopcoadj2i  28345  unierri  28347  branmfn  28348  pjbdlni  28392  pjclem2  28439  sto1i  28479  stm1ri  28487  st0  28492  hstrlem3a  28503  hstrlem4  28505  golem1  28514  superpos  28597  shatomistici  28604  iuninc  28761  hashunif  28949  rhmopp  29150  xrge0slmod  29175  pmtrprfv2  29179  psgnfzto1st  29186  lmatfvlem  29209  lmat22e11  29212  madjusmdetlem1  29221  sqsscirc1  29282  ordtrest2NEW  29297  lmlim  29321  qqh0  29356  qqh1  29357  qqhcn  29363  qqhucn  29364  rrhcn  29369  cnrrext  29382  rrhre  29393  brsigarn  29574  sxval  29580  measvuni  29604  measunl  29606  measinblem  29610  volmeas  29621  braew  29632  aean  29634  sxbrsigalem3  29661  sxbrsiga  29679  0elcarsg  29696  inelcarsg  29700  carsgclctunlem1  29706  carsgclctunlem2  29708  omsmeas  29712  sitgval  29721  sitgclg  29731  sitmcl  29740  eulerpart  29771  fiblem  29787  fibp1  29790  fib2  29791  fib3  29792  fib4  29793  fib5  29794  fib6  29795  probdif  29809  probfinmeasbOLD  29817  cndprobnul  29826  bayesth  29828  dstrvprob  29860  coinflipprob  29868  coinflippvt  29873  ballotlem1  29875  ballotlem2  29877  ballotlemfval0  29884  ballotlem4  29887  ballotlemi1  29891  ballotlemii  29892  ballotlemic  29895  ballotlem1c  29896  ballotlemgun  29913  ballotth  29926  ccatmulgnn0dir  29945  signstfveq0  29980  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  derang0  30405  subfac0  30413  subfac1  30414  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  kur14lem6  30447  kur14lem7  30448  cvmliftlem5  30525  cvmliftlem10  30530  cvmliftlem13  30532  cvmlift2lem9  30547  cvmliftphtlem  30553  msubff1  30707  iexpire  30874  rdgprc0  30943  rankaltopb  31256  rankeq1o  31448  clsun  31493  istoprelowl  32384  finxp1o  32405  finxpreclem4  32407  lindsdom  32573  matunitlindflem1  32575  ptrecube  32579  poimirlem3  32582  poimirlem4  32583  poimirlem30  32609  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  voliunnfl  32623  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  dvasin  32666  dvacos  32667  dvreasin  32668  dvreacos  32669  areacirclem4  32673  fdc  32711  prdsbnd2  32764  ismtyres  32777  reheibor  32808  rngo1cl  32908  rngokerinj  32944  riotaclbgBAD  33258  pmapglb  34074  trlcocnv  35026  dicval2  35486  dicopelval2  35488  dicelval2N  35489  djhfval  35704  djhcom  35712  dihjatcclem1  35725  dihjatcclem2  35726  dihprrnlem1N  35731  dihprrnlem2  35732  djhlsmat  35734  dvh4dimlem  35750  dvh2dim  35752  dvh3dim3N  35756  lclkrlem2c  35816  lclkrlem2m  35826  lclkrlem2v  35835  lcfrlem2  35850  lcfrlem18  35867  lcfrlem21  35870  lcfrlem23  35872  mapdindp4  36030  mapdh6eN  36047  mapdh7dN  36057  mapdh8ab  36084  mapdh8ad  36086  mapdh8b  36087  mapdh8e  36091  hdmap1l6e  36122  hdmapfval  36137  hdmapip1  36226  mapfzcons  36297  mzpresrename  36331  mzpcompact2lem  36332  diophren  36395  rabren3dioph  36397  monotoddzzfi  36525  jm2.23  36581  expdiophlem1  36606  dnnumch1  36632  aomclem6  36647  dfac21  36654  lnrfg  36708  mendsca  36778  mendvscafval  36779  cytpval  36806  arearect  36820  comptiunov2i  37017  trclfvdecomr  37039  ntrclscls00  37384  hashnzfz  37541  hashnzfz2  37542  dvradcnv2  37568  binomcxplemnotnn0  37577  rfcnpre3  38215  rfcnpre4  38216  fprodabs2  38662  mccl  38665  lptioo2cn  38712  lptioo1cn  38713  limclner  38718  cosnegpi  38750  dvnmul  38833  iblempty  38857  iblsplit  38858  stoweidlem11  38904  stoweidlem14  38907  wallispilem3  38960  wallispilem4  38961  wallispi2lem2  38965  dirkerper  38989  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem62  39061  fourierdlem69  39068  fourierdlem73  39072  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem93  39092  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem103  39102  fourierdlem104  39103  fourierdlem108  39107  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  fouriersw  39124  etransclem23  39150  rrxtopn0  39189  sge0tsms  39273  sge0splitmpt  39304  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0isum  39320  sge0xaddlem2  39327  sge0xadd  39328  meaunle  39357  psmeasure  39364  meaiininclem  39376  meaiininc  39377  caragen0  39396  caragenuncllem  39402  omeiunltfirp  39409  ovnsubadd  39462  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem3  39487  hoidmvlelem5  39489  hoidmvle  39490  hspmbllem2  39517  ovnsplit  39538  ovnovollem3  39548  vonioolem2  39572  vonct  39584  smflimlem4  39660  iccpartigtl  39961  iccpartlt  39962  fmtnorec2  39993  fmtno5  40007  nnsum4primeseven  40216  usgrexmpllem  40484  uhgrspan1lem2  40525  uhgrspan1lem3  40526  upgrres1lem2  40530  upgrres1lem3  40531  cusgrsizeinds  40668  cusgrsize  40670  vtxdg0e  40689  uspgrloopvtx  40731  uspgrloopiedg  40733  uspgrloopedg  40734  umgr2v2evtx  40737  umgr2v2eiedg  40739  1wlkres  40879  1wlkp1lem2  40883  trlreslem  40907  crctcshlem2  41021  crctcsh1wlkn0  41024  wlknwwlksnsur  41087  wlkwwlksur  41094  21wlkdlem1  41132  21wlkdlem2  41133  21wlkdlem4  41135  2pthdlem1  41137  21wlkond  41144  2pthd  41147  umgr2adedgwlk  41152  clwwlknclwwlkdifnum  41182  clwlksfclwwlk1hashn  41266  clwlksfoclwwlk  41270  0wlkOn  41288  0clWlk  41298  1pthdlem1  41302  1pthdlem2  41303  11wlkdlem1  41304  11wlkdlem4  41307  1pthond  41311  lp1cycl  41319  1wlk2v2elem2  41323  1wlk2v2e  41324  31wlkdlem1  41326  31wlkdlem2  41327  31wlkdlem4  41329  3pthdlem1  41331  31wlkond  41338  3pthd  41341  3cycld  41345  3cyclpd  41346  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupth2eucrct  41385  eupthvdres  41403  eupth2lem3  41404  eucrct2eupth  41413  konigsbergvtx  41414  konigsbergiedg  41415  konigsberg-av  41427  av-numclwwlkovf2num  41516  av-frgrareg  41548  cznrnglem  41745  cznabel  41746  cznrng  41747  cznnring  41748  rhmsubclem3  41880  rhmsubclem4  41881  rhmsubcALTVlem3  41899  ply1mulgsum  41972  lineval  41976  lcoop  41994  lincfsuppcl  41996  lincvalsng  41999  lincvalpr  42001  lincvalsc0  42004  linc0scn0  42006  lincdifsn  42007  linc1  42008  lincsum  42012  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  snlindsntor  42054  lincresunit3lem2  42063  lincresunit3  42064  zlmodzxzldeplem3  42085  ldepsnlinc  42091  blen1  42176  blen2  42177  aacllem  42356