Theorem fveq2i 5489

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 5486	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( F ` B )

Syntax hints:   = wceq 1343   ` cfv 5188

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 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196

This theorem is referenced by:  fveq12i  5492  ot1stg  6120  ot2ndg  6121  ot3rdgg  6122  algrflem  6197  tfr2a  6289  tfr0dm  6290  tfr0  6291  infisoti  6997  1prl  7496  1pru  7497  ltexprlemell  7539  ltexprlemelu  7540  recexprlemell  7563  recexprlemelu  7564  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  cauappcvgprlem2  7601  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlem2  7621  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemexbt  7647  caucvgprprlem2  7651  suplocexprlem2b  7655  suplocexprlemlub  7665  caucvgsr  7743  axcaucvg  7841  infrenegsupex  9532  fseq1p1m1  10029  fz0to4untppr  10059  rebtwn2zlemstep  10188  rebtwn2z  10190  fldiv4p1lem1div2  10240  frec2uzsucd  10336  frec2uzrdg  10344  frecuzrdgsuc  10349  frecuzrdgg  10351  frecuzrdgsuctlem  10358  frecfzennn  10361  0tonninf  10374  1tonninf  10375  seq3val  10393  seqvalcd  10394  facp1  10643  fac2  10644  fac3  10645  fac4  10646  4bc2eq6  10687  fihasheq0  10707  hashprg  10721  hashp1i  10723  pr0hash2ex  10728  hashfzo  10735  hashxp  10739  zfz1isolemsplit  10751  rei  10841  imi  10842  sqrt1  10988  sqrt4  10989  sqrt9  10990  abs0  11000  absi  11001  infxrnegsupex  11204  fsumabs  11406  fsumrelem  11412  hashrabrex  11422  hashuni  11423  isumnn0nn  11434  mertenslem2  11477  ege2le3  11612  efsep  11632  efgt1p2  11636  efgt1p  11637  sin0  11670  cos0  11671  ef01bndlem  11697  cos2bnd  11701  sin4lt0  11707  eucalg  11991  prmind2  12052  dfphi2  12152  phiprmpw  12154  phimullem  12157  pockthlem  12286  pockthg  12287  prmunb  12292  ennnfonelemjn  12335  ennnfonelem1  12340  ennnfonelemhf1o  12346  sn0cld  12777  txval  12895  hmeontr  12953  comet  13139  cnmetdval  13169  sinhalfpilem  13352  cospi  13361  sincos4thpi  13401  sincos6thpi  13403  sincos3rdpi  13404  sinkpi  13408  reeflog  13424  logbleb  13519  logblt  13520  sqrt2cxp2logb9e3  13533  lgsval2lem  13551  ex-ceil  13607  ex-fac  13609  012of  13875  2o01f  13876  nninfsellemqall  13895  nninfomni  13899  nninffeq  13900  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931