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  6315  ot2ndg  6316  ot3rdgg  6317  algrflem  6394  tfr2a  6487  tfr0dm  6488  tfr0  6489  infisoti  7231  1prl  7775  1pru  7776  ltexprlemell  7818  ltexprlemelu  7819  recexprlemell  7842  recexprlemelu  7843  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlem2b  7934  suplocexprlemlub  7944  caucvgsr  8022  axcaucvg  8120  infrenegsupex  9828  fseq1p1m1  10329  fz0to4untppr  10359  rebtwn2zlemstep  10513  rebtwn2z  10515  fldiv4p1lem1div2  10566  frec2uzsucd  10664  frec2uzrdg  10672  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdgsuctlem  10686  frecfzennn  10689  0tonninf  10703  1tonninf  10704  seq3val  10723  seqvalcd  10724  seqf1oglem2  10783  facp1  10993  fac2  10994  fac3  10995  fac4  10996  4bc2eq6  11037  fihasheq0  11056  hashprg  11073  hashp1i  11075  pr0hash2ex  11080  hashfzo  11087  hashxp  11091  zfz1isolemsplit  11103  hashtpgim  11110  hashtpg  11112  cats1lend  11352  rei  11464  imi  11465  sqrt1  11611  sqrt4  11612  sqrt9  11613  abs0  11623  absi  11624  infxrnegsupex  11828  fsumabs  12031  fsumrelem  12037  hashrabrex  12047  hashuni  12048  isumnn0nn  12059  mertenslem2  12102  ege2le3  12237  efsep  12257  efgt1p2  12261  efgt1p  12262  sin0  12295  cos0  12296  ef01bndlem  12322  cos2bnd  12326  sin4lt0  12333  m1bits  12526  nninfctlemfo  12616  eucalg  12636  prmind2  12697  dfphi2  12797  phiprmpw  12799  phimullem  12802  pockthlem  12934  pockthg  12935  prmunb  12940  ennnfonelemjn  13028  ennnfonelem1  13033  ennnfonelemhf1o  13039  imasplusg  13396  ringidvalg  13980  rmodislmod  14371  lspprid2  14432  sn0cld  14867  txval  14985  hmeontr  15043  comet  15229  cnmetdval  15259  sinhalfpilem  15521  cospi  15530  sincos4thpi  15570  sincos6thpi  15572  sincos3rdpi  15573  sinkpi  15577  reeflog  15593  logbleb  15691  logblt  15692  sqrt2cxp2logb9e3  15705  lgsval2lem  15745  lgsquadlem2  15813  setsiedg  15909  wlkres  16236  trlreslem  16246  clwwlkccatlem  16257  eupthvdres  16332  eupth2lem3fi  16333  ex-ceil  16344  ex-fac  16346  012of  16618  2o01f  16619  nninfsellemqall  16643  nninfomni  16647  nninffeq  16648  isomninnlem  16660  iswomninnlem  16680  ismkvnnlem  16683  gfsump1  16713