Theorem fveq2i 5642

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

Syntax hints:   = wceq 1397  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq12i  5645  ot1stg  6314  ot2ndg  6315  ot3rdgg  6316  algrflem  6393  tfr2a  6486  tfr0dm  6487  tfr0  6488  infisoti  7230  1prl  7774  1pru  7775  ltexprlemell  7817  ltexprlemelu  7818  recexprlemell  7841  recexprlemelu  7842  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocexprlem2b  7933  suplocexprlemlub  7943  caucvgsr  8021  axcaucvg  8119  infrenegsupex  9827  fseq1p1m1  10328  fz0to4untppr  10358  rebtwn2zlemstep  10511  rebtwn2z  10513  fldiv4p1lem1div2  10564  frec2uzsucd  10662  frec2uzrdg  10670  frecuzrdgsuc  10675  frecuzrdgg  10677  frecuzrdgsuctlem  10684  frecfzennn  10687  0tonninf  10701  1tonninf  10702  seq3val  10721  seqvalcd  10722  seqf1oglem2  10781  facp1  10991  fac2  10992  fac3  10993  fac4  10994  4bc2eq6  11035  fihasheq0  11054  hashprg  11071  hashp1i  11073  pr0hash2ex  11078  hashfzo  11085  hashxp  11089  zfz1isolemsplit  11101  cats1lend  11347  rei  11459  imi  11460  sqrt1  11606  sqrt4  11607  sqrt9  11608  abs0  11618  absi  11619  infxrnegsupex  11823  fsumabs  12025  fsumrelem  12031  hashrabrex  12041  hashuni  12042  isumnn0nn  12053  mertenslem2  12096  ege2le3  12231  efsep  12251  efgt1p2  12255  efgt1p  12256  sin0  12289  cos0  12290  ef01bndlem  12316  cos2bnd  12320  sin4lt0  12327  m1bits  12520  nninfctlemfo  12610  eucalg  12630  prmind2  12691  dfphi2  12791  phiprmpw  12793  phimullem  12796  pockthlem  12928  pockthg  12929  prmunb  12934  ennnfonelemjn  13022  ennnfonelem1  13027  ennnfonelemhf1o  13033  imasplusg  13390  ringidvalg  13973  rmodislmod  14364  lspprid2  14425  sn0cld  14860  txval  14978  hmeontr  15036  comet  15222  cnmetdval  15252  sinhalfpilem  15514  cospi  15523  sincos4thpi  15563  sincos6thpi  15565  sincos3rdpi  15566  sinkpi  15570  reeflog  15586  logbleb  15684  logblt  15685  sqrt2cxp2logb9e3  15698  lgsval2lem  15738  lgsquadlem2  15806  setsiedg  15902  wlkres  16229  trlreslem  16239  clwwlkccatlem  16250  ex-ceil  16322  ex-fac  16324  012of  16592  2o01f  16593  nninfsellemqall  16617  nninfomni  16621  nninffeq  16622  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656