Theorem fveq2i 5638

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

Syntax hints:   = wceq 1395  ‘cfv 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  fveq12i  5641  ot1stg  6310  ot2ndg  6311  ot3rdgg  6312  algrflem  6389  tfr2a  6482  tfr0dm  6483  tfr0  6484  infisoti  7222  1prl  7765  1pru  7766  ltexprlemell  7808  ltexprlemelu  7809  recexprlemell  7832  recexprlemelu  7833  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocexprlem2b  7924  suplocexprlemlub  7934  caucvgsr  8012  axcaucvg  8110  infrenegsupex  9818  fseq1p1m1  10319  fz0to4untppr  10349  rebtwn2zlemstep  10502  rebtwn2z  10504  fldiv4p1lem1div2  10555  frec2uzsucd  10653  frec2uzrdg  10661  frecuzrdgsuc  10666  frecuzrdgg  10668  frecuzrdgsuctlem  10675  frecfzennn  10678  0tonninf  10692  1tonninf  10693  seq3val  10712  seqvalcd  10713  seqf1oglem2  10772  facp1  10982  fac2  10983  fac3  10984  fac4  10985  4bc2eq6  11026  fihasheq0  11045  hashprg  11062  hashp1i  11064  pr0hash2ex  11069  hashfzo  11076  hashxp  11080  zfz1isolemsplit  11092  cats1lend  11338  rei  11450  imi  11451  sqrt1  11597  sqrt4  11598  sqrt9  11599  abs0  11609  absi  11610  infxrnegsupex  11814  fsumabs  12016  fsumrelem  12022  hashrabrex  12032  hashuni  12033  isumnn0nn  12044  mertenslem2  12087  ege2le3  12222  efsep  12242  efgt1p2  12246  efgt1p  12247  sin0  12280  cos0  12281  ef01bndlem  12307  cos2bnd  12311  sin4lt0  12318  m1bits  12511  nninfctlemfo  12601  eucalg  12621  prmind2  12682  dfphi2  12782  phiprmpw  12784  phimullem  12787  pockthlem  12919  pockthg  12920  prmunb  12925  ennnfonelemjn  13013  ennnfonelem1  13018  ennnfonelemhf1o  13024  imasplusg  13381  ringidvalg  13964  rmodislmod  14355  lspprid2  14416  sn0cld  14851  txval  14969  hmeontr  15027  comet  15213  cnmetdval  15243  sinhalfpilem  15505  cospi  15514  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  sinkpi  15561  reeflog  15577  logbleb  15675  logblt  15676  sqrt2cxp2logb9e3  15689  lgsval2lem  15729  lgsquadlem2  15797  setsiedg  15893  wlkres  16174  trlreslem  16184  clwwlkccatlem  16195  ex-ceil  16258  ex-fac  16260  012of  16528  2o01f  16529  nninfsellemqall  16553  nninfomni  16557  nninffeq  16558  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592