Theorem fveq2i 5642

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 5639	. 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  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  10512  rebtwn2z  10514  fldiv4p1lem1div2  10565  frec2uzsucd  10663  frec2uzrdg  10671  frecuzrdgsuc  10676  frecuzrdgg  10678  frecuzrdgsuctlem  10685  frecfzennn  10688  0tonninf  10702  1tonninf  10703  seq3val  10722  seqvalcd  10723  seqf1oglem2  10782  facp1  10992  fac2  10993  fac3  10994  fac4  10995  4bc2eq6  11036  fihasheq0  11055  hashprg  11072  hashp1i  11074  pr0hash2ex  11079  hashfzo  11086  hashxp  11090  zfz1isolemsplit  11102  cats1lend  11348  rei  11460  imi  11461  sqrt1  11607  sqrt4  11608  sqrt9  11609  abs0  11619  absi  11620  infxrnegsupex  11824  fsumabs  12027  fsumrelem  12033  hashrabrex  12043  hashuni  12044  isumnn0nn  12055  mertenslem2  12098  ege2le3  12233  efsep  12253  efgt1p2  12257  efgt1p  12258  sin0  12291  cos0  12292  ef01bndlem  12318  cos2bnd  12322  sin4lt0  12329  m1bits  12522  nninfctlemfo  12612  eucalg  12632  prmind2  12693  dfphi2  12793  phiprmpw  12795  phimullem  12798  pockthlem  12930  pockthg  12931  prmunb  12936  ennnfonelemjn  13024  ennnfonelem1  13029  ennnfonelemhf1o  13035  imasplusg  13392  ringidvalg  13976  rmodislmod  14367  lspprid2  14428  sn0cld  14863  txval  14981  hmeontr  15039  comet  15225  cnmetdval  15255  sinhalfpilem  15517  cospi  15526  sincos4thpi  15566  sincos6thpi  15568  sincos3rdpi  15569  sinkpi  15573  reeflog  15589  logbleb  15687  logblt  15688  sqrt2cxp2logb9e3  15701  lgsval2lem  15741  lgsquadlem2  15809  setsiedg  15905  wlkres  16232  trlreslem  16242  clwwlkccatlem  16253  ex-ceil  16325  ex-fac  16327  012of  16595  2o01f  16596  nninfsellemqall  16620  nninfomni  16624  nninffeq  16625  isomninnlem  16637  iswomninnlem  16656  ismkvnnlem  16659  gfsump1  16689