Theorem fveq2i 6673

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 6670	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1537  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  fveq12i  6676  ot1stg  7703  ot2ndg  7704  ot3rdg  7705  algrflem  7819  wfrlem5  7959  wfrlem14  7968  tfr2a  8031  rdgsucmptf  8064  rdgsucmptnf  8065  frsucmpt  8073  frsucmptn  8074  infiso  8972  inf3lemc  9089  cantnf  9156  wemapwe  9160  cnfcom2lem  9164  cnfcom2  9165  cnfcom3lem  9166  r1sucg  9198  rankprb  9280  rankopb  9281  ranksuc  9294  rankmapu  9307  cardiun  9411  alephsuc  9494  alephcard  9496  alephfplem2  9531  ackbij1lem8  9649  ackbij1lem13  9654  ackbij1lem14  9655  ackbij2lem2  9662  infpssrlem2  9726  fin23lem34  9768  fin23lem35  9769  aleph1  9993  pwcfsdom  10005  cfpwsdom  10006  alephom  10007  rankcf  10199  addpqnq  10360  mulpqnq  10363  addcomnq  10373  mulcomnq  10375  addclprlem2  10439  infrenegsup  11624  fseq1p1m1  12982  fz0to4untppr  13011  fldiv4p1lem1div2  13206  om2uzrdg  13325  uzrdgsuci  13329  fzennn  13337  axdc4uzlem  13352  seqp1i  13387  seqf1olem2  13411  facp1  13639  fac2  13640  fac3  13641  fac4  13642  4bc2eq6  13690  hashcard  13717  hasheq0  13725  hashun2  13745  hashun3  13746  hashprg  13757  hashprb  13759  hashprdifel  13760  hashp1i  13765  pr0hash2ex  13770  hashdif  13775  hashunlei  13787  hashfzo  13791  hashxplem  13795  hashfun  13799  hashimarn  13802  hashbclem  13811  hashbc  13812  hashf1lem2  13815  hashtpg  13844  ccatalpha  13947  s1len  13960  ccat2s1p2  13986  revs1  14127  cats1len  14222  lsws2  14266  lsws3  14267  lsws4  14268  rei  14515  imi  14516  sqrt1  14631  sqrt4  14632  sqrt9  14633  abs0  14645  absi  14646  sqreulem  14719  fsumabs  15156  fsumrelem  15162  o1fsum  15168  hashrabrex  15180  hashuni  15181  incexclem  15191  incexc  15192  isumnn0nn  15197  fprodefsum  15448  efsep  15463  sin0  15502  cos0  15503  ef01bndlem  15537  cos2bnd  15541  sin4lt0  15548  ruclem6  15588  aleph1re  15598  pwp1fsum  15742  m1bits  15789  sadcaddlem  15806  sadaddlem  15815  sadeq  15821  algrp1  15918  eucalg  15931  prmind2  16029  dfphi2  16111  phiprmpw  16113  phimullem  16116  pockthlem  16241  pockthg  16242  prmunb  16250  prmreclem4  16255  vdwap1  16313  vdwlem12  16328  prmo2  16376  prmo3  16377  prmgaplem7  16393  prmo4  16461  prmo5  16462  prmo6  16463  imasvsca  16793  mreexdomd  16920  isoval  17035  yonedalem21  17523  yonedalem22  17528  joincomALT  17639  meetcomALT  17641  lubsn  17704  oduleval  17741  odubas  17743  isacs5lem  17779  acsmapd  17788  efmnd1hash  18057  efmnd1bas  18058  efmnd2hash  18059  oppgplusfval  18476  oppglem  18478  symgbas  18499  symghash  18506  symgplusg  18511  symg1hash  18518  symg2hash  18520  symgtset  18527  symggen  18598  psgnsn  18648  psgnprfval1  18650  psgnprfval2  18651  odngen  18702  sylow1lem1  18723  efgs1b  18862  efgsfo  18865  efgredlemg  18868  efgredlemd  18870  frgpuplem  18898  gsumzmhm  19057  gsumzinv  19065  dprd2da  19164  dmdprdsplit2lem  19167  pgpfaclem1  19203  mgpplusg  19243  mgplem  19244  ringidval  19253  opprmulfval  19375  opprlem  19378  isrhm2d  19480  rhm1  19482  subdrgint  19582  rmodislmod  19702  lspprid2  19770  lsmpr  19861  lsppr  19865  lspsntri  19869  lbspropd  19871  lspexchn2  19903  lspindp2l  19906  lspindp2  19907  lspsnat  19917  lsppratlem1  19919  lsppratlem3  19921  lsppratlem4  19922  lidlrsppropd  20003  assamulgscmlem2  20129  evlsval  20299  selvval  20331  psropprmul  20406  ply1sca2  20422  ply1mpl0  20423  ply1mpl1  20425  coe1fzgsumd  20470  evls1var  20501  evl1gsumd  20520  evl1varpw  20524  evl1varpwval  20525  evl1scvarpw  20526  zrhpsgnodpm  20736  psgnfix1  20742  psgnfix2  20743  psgndiflemB  20744  dsmmbas2  20881  dsmmelbas  20883  dsmmsubg  20887  frlmip  20922  islinds2  20957  lindsind2  20963  lindfmm  20971  islindf4  20982  mat1bas  21058  mat0dim0  21076  mat0dimid  21077  mat0dimscm  21078  mat0dimcrng  21079  mat1rhmelval  21089  dmatval  21101  scmatval  21113  mat1scmat  21148  1mavmul  21157  marrepfval  21169  marepvfval  21174  ma1repvcl  21179  ma1repveval  21180  submafval  21188  mdetfval1  21199  mdetralt  21217  mdetunilem7  21227  m2detleiblem3  21238  m2detleiblem4  21239  madufval  21246  maducoeval2  21249  madugsum  21252  minmar1fval  21255  cramerimplem1  21292  cramer0  21299  pmatcoe1fsupp  21309  cpmat  21317  mat2pmatfval  21331  mat2pmatmul  21339  idmatidpmat  21345  m2cpminv0  21369  pmatcollpwfi  21390  pmatcollpw3fi1lem1  21394  pm2mpval  21403  chpmatval2  21441  cpmidpmat  21481  cayleyhamilton1  21500  sn0cld  21698  lpdifsn  21751  restcls  21789  restntr  21790  ordtrest2  21812  leordtval  21821  pttoponconst  22205  ptclsg  22223  xkoptsub  22262  xkofvcn  22292  tgqtop  22320  hmeocls  22376  hmeontr  22377  ptcmpfi  22421  ptcmplem1  22660  tmdgsum  22703  utop2nei  22859  cuspcvg  22910  iscusp2  22911  cnextucn  22912  comet  23123  nrmmetd  23184  isngp3  23207  ngpds  23213  tngnm  23260  cnmetdval  23379  qdensere2  23405  tgioo3  23413  cnmpopc  23532  cnheibor  23559  htpyco2  23583  phtpyco2  23594  pco0  23618  pi1xfrcnv  23661  cnrbas  23746  cncvs  23749  cnnm  23764  ipcau2  23837  cfilfcls  23877  cncmet  23925  reust  23984  rrxprds  23992  rrxsca  23999  ehleudis  24021  ehleudisval  24022  pjthlem1  24040  ovolunlem1a  24097  ovolfiniun  24102  ovoliunlem2  24104  ovoliunlem3  24105  ovoliun  24106  ovolicc1  24117  ismbl2  24128  unmbl  24138  volinun  24147  volfiniun  24148  voliunlem1  24151  voliunlem2  24152  ioorinv  24177  mbfimaopnlem  24256  itg2cnlem2  24363  itg2cn  24364  dfitg  24370  itg0  24380  iblre  24394  itgreval  24397  itgitg2  24407  iblconst  24418  itgconst  24419  itgcn  24443  limcflflem  24478  dvn1  24523  dvlipcn  24591  c1lip2  24595  dvcnvrelem2  24615  ply1divalg2  24732  ply1remlem  24756  dgr0  24852  elqaalem2  24909  dvradcnv  25009  pserdvlem2  25016  pserdv2  25018  abelthlem6  25024  abelthlem9  25028  sinhalfpilem  25049  cospi  25058  sincos4thpi  25099  sincos6thpi  25101  sincos3rdpi  25102  pige3ALT  25105  sinkpi  25107  eflog  25160  logfac  25184  logdmopn  25232  logtayl  25243  cxpcn3  25329  root1eq1  25336  cxpeq  25338  logbleb  25361  logblt  25362  sqrt2cxp2logb9e3  25377  ang180lem1  25387  ang180lem2  25388  ang180lem4  25390  lawcos  25394  1cubrlem  25419  asin1  25472  atan0  25486  atan1  25506  log2cnv  25522  birthdaylem2  25530  lgamgulmlem2  25607  gam1  25642  ftalem3  25652  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  ppi1  25741  ppi1i  25745  ppi2i  25746  cht2  25749  cht3  25750  ppiub  25780  chtub  25788  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgsval2lem  25883  lgsqrlem1  25922  lgsqrlem4  25925  lgsquadlem2  25957  chebbnd1  26048  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0flb  26086  mulog2sumlem2  26111  pntpbnd1a  26161  pntlemf  26181  cchhllem  26673  axlowdimlem17  26744  graop  26814  setsiedg  26821  vtxvalsnop  26826  iedgvalsnop  26827  usgrexmpllem  27042  uhgrspan1lem2  27083  uhgrspan1lem3  27084  upgrres1lem2  27093  upgrres1lem3  27094  structtocusgr  27228  cusgrsizeinds  27234  cusgrsize  27236  vtxdg0e  27256  uspgrloopvtx  27297  uspgrloopiedg  27299  uspgrloopedg  27300  umgr2v2evtx  27303  umgr2v2eiedg  27305  vtxdginducedm1lem1  27321  vtxdginducedm1  27325  vtxdginducedm1fi  27326  finsumvtxdg2ssteplem1  27327  finsumvtxdg2ssteplem2  27328  finsumvtxdg2ssteplem3  27329  finsumvtxdg2ssteplem4  27330  finsumvtxdg2sstep  27331  finsumvtxdg2size  27332  wlkres  27452  wlkp1lem2  27456  trlreslem  27481  clwlkcompbp  27563  crctcshlem2  27596  crctcshwlkn0  27599  2wlkdlem1  27704  2wlkdlem2  27705  2wlkdlem4  27707  2pthdlem1  27709  2wlkond  27716  2pthd  27719  umgr2adedgwlk  27724  clwwlknclwwlkdifnum  27758  clwwlkccatlem  27767  clwlkclwwlkfo  27787  clwlknf1oclwwlkn  27863  clwwlknon2num  27884  0wlkon  27899  0clwlk  27909  0cycl  27913  1pthdlem1  27914  1pthdlem2  27915  1wlkdlem1  27916  1wlkdlem4  27919  1pthond  27923  lp1cycl  27931  wlk2v2elem2  27935  wlk2v2e  27936  3wlkdlem1  27938  3wlkdlem2  27939  3wlkdlem4  27941  3pthdlem1  27943  3wlkond  27950  3pthd  27953  3cycld  27957  3cyclpd  27958  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth2eucrct  27996  eupthvdres  28014  eupth2lem3  28015  eucrct2eupth  28024  konigsbergvtx  28025  konigsbergiedg  28026  konigsberg  28036  2clwwlk2  28127  numclwlk1lem1  28148  numclwlk1  28150  numclwwlkqhash  28154  frgrreg  28173  ex-co  28217  ex-ceil  28227  ex-fac  28230  ex-hash  28232  ex-sqrt  28233  ex-prmo  28238  0vfval  28383  nvvop  28386  vsfval  28410  cnnvg  28455  cnnvs  28457  cnnvnm  28458  imsdval  28463  ipidsq  28487  nmblolbii  28576  blocnilem  28581  ip0i  28602  ip1ilem  28603  ipasslem10  28616  siilem1  28628  cnbn  28646  h2hva  28751  h2hsm  28752  h2hnm  28753  axhfvadd-zf  28759  axhvcom-zf  28760  axhvass-zf  28761  axhv0cl-zf  28762  axhvaddid-zf  28763  axhfvmul-zf  28764  axhvmulid-zf  28765  axhvmulass-zf  28766  axhvdistr1-zf  28767  axhvdistr2-zf  28768  axhvmul0-zf  28769  axhfi-zf  28770  axhis1-zf  28771  axhis2-zf  28772  axhis3-zf  28773  axhis4-zf  28774  axhcompl-zf  28775  norm-iii-i  28916  normsubi  28918  norm3difi  28924  normpar2i  28933  hh0v  28945  hhssva  29034  hhsssm  29035  hhssnm  29036  hhshsslem1  29044  hhsscms  29055  choc1  29104  shjcom  29135  pjhthlem1  29168  pjoc2i  29215  shs0i  29226  chj0i  29232  chdmj1i  29258  chjassi  29263  spansn0  29318  spanpr  29357  qlaxr4i  29411  pjadjii  29451  pjaddii  29452  pjmulii  29454  pjsubii  29455  pjcji  29461  pjnormi  29498  pjpythi  29499  ho0val  29527  lnop0  29743  lnophmlem2  29794  nmbdoplbi  29801  nmcopexi  29804  lnfn0i  29819  nmcfnexi  29828  nmopadji  29867  nmoptri2i  29876  nmopcoadj2i  29879  unierri  29881  branmfn  29882  pjbdlni  29926  pjclem2  29973  sto1i  30013  stm1ri  30021  st0  30026  hstrlem3a  30037  hstrlem4  30039  golem1  30048  superpos  30131  shatomistici  30138  iuninc  30312  hashunif  30528  pfxlsw2ccat  30626  pmtrprfv2  30732  psgnfzto1st  30747  cyc2fv1  30763  cycpmco2lem4  30771  cycpmco2lem7  30774  cycpmco2  30775  cyc3fv1  30779  cyc3fv2  30780  cycpmrn  30785  cyc3genpmlem  30793  primefldchr  30867  rhmopp  30892  xrge0slmod  30917  rgmoddim  31008  lbslsat  31014  lindsun  31021  ccfldextdgrr  31057  lmatfvlem  31080  lmat22e11  31083  madjusmdetlem1  31092  sqsscirc1  31151  ordtrest2NEW  31166  lmlim  31190  qqh0  31225  qqh1  31226  qqhcn  31232  qqhucn  31233  rrhcn  31238  cnrrext  31251  rrhre  31262  brsigarn  31443  sxval  31449  measvuni  31473  measunl  31475  measinblem  31479  volmeas  31490  braew  31501  aean  31503  sxbrsigalem3  31530  sxbrsiga  31548  0elcarsg  31565  inelcarsg  31569  carsgclctunlem1  31575  carsgclctunlem2  31577  omsmeas  31581  sitgval  31590  sitgclg  31600  sitmcl  31609  eulerpart  31640  fiblem  31656  fibp1  31659  fib2  31660  fib3  31661  fib4  31662  fib5  31663  fib6  31664  probdif  31678  probfinmeasbALTV  31687  cndprobnul  31695  bayesth  31697  dstrvprob  31729  coinflipprob  31737  coinflippvt  31742  ballotlem1  31744  ballotlem2  31746  ballotlemfval0  31753  ballotlem4  31756  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  ballotlemgun  31782  ballotth  31795  ccatmulgnn0dir  31812  signstfveq0  31847  signsvtp  31853  signsvtn  31854  signsvfpn  31855  signsvfnn  31856  ftc2re  31869  hgt750lemd  31919  hgt750lem  31922  2cycld  32385  derang0  32416  subfac0  32424  subfac1  32425  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  kur14lem6  32458  kur14lem7  32459  cvmliftlem5  32536  cvmliftlem10  32541  cvmliftlem13  32543  cvmlift2lem9  32558  cvmliftphtlem  32564  satfv1  32610  fmla1  32634  satfv0fvfmla0  32660  sategoelfvb  32666  msubff1  32803  iexpire  32967  rdgprc0  33038  nosepne  33185  rankaltopb  33440  rankeq1o  33632  clsun  33676  istoprelowl  34644  finxp1o  34676  finxpreclem4  34678  lindsdom  34901  matunitlindflem1  34903  ptrecube  34907  poimirlem3  34910  poimirlem4  34911  poimirlem30  34937  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  voliunnfl  34951  ftc1anclem3  34984  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  dvasin  34993  dvacos  34994  dvreasin  34995  dvreacos  34996  areacirclem4  35000  fdc  35035  prdsbnd2  35088  ismtyres  35101  reheibor  35132  rngo1cl  35232  rngokerinj  35268  riotaclbgBAD  36105  pmapglb  36921  trlcocnv  37871  dicval2  38330  dicopelval2  38332  dicelval2N  38333  djhfval  38548  djhcom  38556  dihjatcclem1  38569  dihjatcclem2  38570  dihprrnlem1N  38575  dihprrnlem2  38576  djhlsmat  38578  dvh4dimlem  38594  dvh2dim  38596  dvh3dim3N  38600  lclkrlem2c  38660  lclkrlem2m  38670  lclkrlem2v  38679  lcfrlem2  38694  lcfrlem18  38711  lcfrlem21  38714  lcfrlem23  38716  mapdindp4  38874  mapdh6eN  38891  mapdh7dN  38901  mapdh8ab  38928  mapdh8ad  38930  mapdh8b  38931  mapdh8e  38935  hdmap1l6e  38965  hdmapfval  38978  hdmapip1  39067  lcmfunnnd  39133  lcm1un  39134  lcm2un  39135  lcm3un  39136  lcm4un  39137  lcm5un  39138  lcm6un  39139  lcm7un  39140  lcm8un  39141  prjspnval2  39316  mapfzcons  39362  mzpresrename  39396  mzpcompact2lem  39397  diophren  39459  rabren3dioph  39461  monotoddzzfi  39588  jm2.23  39642  expdiophlem1  39667  dnnumch1  39693  aomclem6  39708  dfac21  39715  lnrfg  39768  mendsca  39838  mendvscafval  39839  cytpval  39858  arearect  39871  aleph1min  39965  comptiunov2i  40100  trclfvdecomr  40122  ntrclscls00  40465  hashnzfz  40701  hashnzfz2  40702  dvradcnv2  40728  binomcxplemnotnn0  40737  rfcnpre3  41339  rfcnpre4  41340  fprodabs2  41925  mccl  41928  lptioo2cn  41975  lptioo1cn  41976  limclner  41981  limsupresuz  42033  limsupequzmpt2  42048  limsupequzmptf  42061  climlimsupcex  42099  liminfresre  42109  liminfvalxr  42113  liminfresuz  42114  liminfequzmpt2  42121  liminf0  42123  liminfpnfuz  42146  cosnegpi  42197  dvnmul  42277  iblempty  42299  iblsplit  42300  stoweidlem11  42345  stoweidlem14  42348  wallispilem3  42401  wallispilem4  42402  wallispi2lem2  42406  dirkerper  42430  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem62  42502  fourierdlem69  42509  fourierdlem73  42513  fourierdlem79  42519  fourierdlem80  42520  fourierdlem81  42521  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem93  42533  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem100  42540  fourierdlem103  42543  fourierdlem104  42544  fourierdlem108  42548  fourierdlem110  42550  fourierdlem112  42552  fourierdlem113  42553  fouriersw  42565  etransclem23  42591  rrxtopn0  42627  sge0tsms  42711  sge0splitmpt  42742  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0isum  42758  sge0xaddlem2  42765  sge0xadd  42766  meaunle  42795  psmeasure  42802  meaiunincf  42814  meaiuninc3  42816  meaiininclem  42817  meaiininc  42818  caragen0  42837  caragenuncllem  42843  omeiunltfirp  42850  ovnsubadd  42903  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem3  42928  hoidmvlelem5  42930  hoidmvle  42931  hspmbllem2  42958  ovnsplit  42979  ovnovollem3  42989  vonioolem2  43012  vonct  43024  smflimlem4  43099  smflimsuplem2  43144  smflimsuplem8  43150  smflimsup  43151  iccpartigtl  43632  iccpartlt  43633  fmtnorec2  43754  fmtno5  43768  nnsum4primeseven  44014  strisomgrop  44054  ushrisomgr  44055  cznrnglem  44273  cznabel  44274  cznrng  44275  cznnring  44276  rhmsubclem3  44408  rhmsubclem4  44409  rhmsubcALTVlem3  44426  ply1mulgsum  44493  lineval  44497  lcoop  44515  lincfsuppcl  44517  lincvalsng  44520  lincvalpr  44522  lincvalsc0  44525  linc0scn0  44527  lincdifsn  44528  linc1  44529  lincsum  44533  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  snlindsntor  44575  lincresunit3lem2  44584  lincresunit3  44585  zlmodzxzldeplem3  44606  ldepsnlinc  44612  blen1  44693  blen2  44694  lines  44767  rrxsphere  44784  2sphere  44785  itscnhlinecirc02plem3  44820  inlinecirc02p  44823  aacllem  44951