Theorem fveq2i 5488

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

Syntax hints:   = wceq 1343  ‘cfv 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195

This theorem is referenced by:  fveq12i  5491  ot1stg  6117  ot2ndg  6118  ot3rdgg  6119  algrflem  6193  tfr2a  6285  tfr0dm  6286  tfr0  6287  infisoti  6993  1prl  7492  1pru  7493  ltexprlemell  7535  ltexprlemelu  7536  recexprlemell  7559  recexprlemelu  7560  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlem2b  7651  suplocexprlemlub  7661  caucvgsr  7739  axcaucvg  7837  infrenegsupex  9528  fseq1p1m1  10025  fz0to4untppr  10055  rebtwn2zlemstep  10184  rebtwn2z  10186  fldiv4p1lem1div2  10236  frec2uzsucd  10332  frec2uzrdg  10340  frecuzrdgsuc  10345  frecuzrdgg  10347  frecuzrdgsuctlem  10354  frecfzennn  10357  0tonninf  10370  1tonninf  10371  seq3val  10389  seqvalcd  10390  facp1  10639  fac2  10640  fac3  10641  fac4  10642  4bc2eq6  10683  fihasheq0  10703  hashprg  10717  hashp1i  10719  pr0hash2ex  10724  hashfzo  10731  hashxp  10735  zfz1isolemsplit  10747  rei  10837  imi  10838  sqrt1  10984  sqrt4  10985  sqrt9  10986  abs0  10996  absi  10997  infxrnegsupex  11200  fsumabs  11402  fsumrelem  11408  hashrabrex  11418  hashuni  11419  isumnn0nn  11430  mertenslem2  11473  ege2le3  11608  efsep  11628  efgt1p2  11632  efgt1p  11633  sin0  11666  cos0  11667  ef01bndlem  11693  cos2bnd  11697  sin4lt0  11703  eucalg  11987  prmind2  12048  dfphi2  12148  phiprmpw  12150  phimullem  12153  pockthlem  12282  pockthg  12283  prmunb  12288  ennnfonelemjn  12331  ennnfonelem1  12336  ennnfonelemhf1o  12342  sn0cld  12737  txval  12855  hmeontr  12913  comet  13099  cnmetdval  13129  sinhalfpilem  13312  cospi  13321  sincos4thpi  13361  sincos6thpi  13363  sincos3rdpi  13364  sinkpi  13368  reeflog  13384  logbleb  13479  logblt  13480  sqrt2cxp2logb9e3  13493  lgsval2lem  13511  ex-ceil  13567  ex-fac  13569  012of  13835  2o01f  13836  nninfsellemqall  13855  nninfomni  13859  nninffeq  13860  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891