Theorem fveq2i 5643

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	|- A = B

Assertion

Ref	Expression
fveq2i	|- ( F ` A ) = ( F ` B )

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 |- A = B
2		fveq2 5640	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( F ` B )

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  5646  ot1stg  6318  ot2ndg  6319  ot3rdgg  6320  algrflem  6397  tfr2a  6490  tfr0dm  6491  tfr0  6492  infisoti  7234  1prl  7778  1pru  7779  ltexprlemell  7821  ltexprlemelu  7822  recexprlemell  7845  recexprlemelu  7846  cauappcvgprlemm  7868  cauappcvgprlemopl  7869  cauappcvgprlemlol  7870  cauappcvgprlemopu  7871  cauappcvgprlemupu  7872  cauappcvgprlemdisj  7874  cauappcvgprlemloc  7875  cauappcvgprlemladdfu  7877  cauappcvgprlemladdfl  7878  cauappcvgprlemladdru  7879  cauappcvgprlem2  7883  caucvgprlemm  7891  caucvgprlemopl  7892  caucvgprlemlol  7893  caucvgprlemopu  7894  caucvgprlemupu  7895  caucvgprlemdisj  7897  caucvgprlemloc  7898  caucvgprlemladdfu  7900  caucvgprlem2  7903  caucvgprprlemell  7908  caucvgprprlemelu  7909  caucvgprprlemml  7917  caucvgprprlemmu  7918  caucvgprprlemexbt  7929  caucvgprprlem2  7933  suplocexprlem2b  7937  suplocexprlemlub  7947  caucvgsr  8025  axcaucvg  8123  infrenegsupex  9831  fseq1p1m1  10332  fz0to4untppr  10362  rebtwn2zlemstep  10516  rebtwn2z  10518  fldiv4p1lem1div2  10569  frec2uzsucd  10667  frec2uzrdg  10675  frecuzrdgsuc  10680  frecuzrdgg  10682  frecuzrdgsuctlem  10689  frecfzennn  10692  0tonninf  10706  1tonninf  10707  seq3val  10726  seqvalcd  10727  seqf1oglem2  10786  facp1  10996  fac2  10997  fac3  10998  fac4  10999  4bc2eq6  11040  fihasheq0  11059  hashprg  11076  hashp1i  11078  pr0hash2ex  11083  hashfzo  11090  hashxp  11094  zfz1isolemsplit  11106  hashtpgim  11113  hashtpg  11115  cats1lend  11355  rei  11480  imi  11481  sqrt1  11627  sqrt4  11628  sqrt9  11629  abs0  11639  absi  11640  infxrnegsupex  11844  fsumabs  12047  fsumrelem  12053  hashrabrex  12063  hashuni  12064  isumnn0nn  12075  mertenslem2  12118  ege2le3  12253  efsep  12273  efgt1p2  12277  efgt1p  12278  sin0  12311  cos0  12312  ef01bndlem  12338  cos2bnd  12342  sin4lt0  12349  m1bits  12542  nninfctlemfo  12632  eucalg  12652  prmind2  12713  dfphi2  12813  phiprmpw  12815  phimullem  12818  pockthlem  12950  pockthg  12951  prmunb  12956  ennnfonelemjn  13044  ennnfonelem1  13049  ennnfonelemhf1o  13055  imasplusg  13412  ringidvalg  13996  rmodislmod  14387  lspprid2  14448  sn0cld  14888  txval  15006  hmeontr  15064  comet  15250  cnmetdval  15280  sinhalfpilem  15542  cospi  15551  sincos4thpi  15591  sincos6thpi  15593  sincos3rdpi  15594  sinkpi  15598  reeflog  15614  logbleb  15712  logblt  15713  sqrt2cxp2logb9e3  15726  lgsval2lem  15766  lgsquadlem2  15834  setsiedg  15930  wlkres  16257  trlreslem  16267  clwwlkccatlem  16278  eupthvdres  16353  eupth2lem3fi  16354  konigsbergvtx  16360  konigsbergiedg  16361  konigsberglem5  16370  konigsberg  16371  ex-ceil  16377  ex-fac  16379  012of  16651  2o01f  16652  nninfsellemqall  16676  nninfomni  16680  nninffeq  16681  isomninnlem  16693  iswomninnlem  16713  ismkvnnlem  16716  gfsump1  16746