Theorem fveq2i 5696

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

Syntax hints:   = wceq 1402   ` cfv 5375

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383

This theorem is referenced by:  fveq12i  5699  ot1stg  6379  ot2ndg  6380  ot3rdgg  6381  algrflem  6458  tfr2a  6585  tfr0dm  6586  tfr0  6587  infisoti  7365  1prl  7915  1pru  7916  ltexprlemell  7958  ltexprlemelu  7959  recexprlemell  7982  recexprlemelu  7983  cauappcvgprlemm  8005  cauappcvgprlemopl  8006  cauappcvgprlemlol  8007  cauappcvgprlemopu  8008  cauappcvgprlemupu  8009  cauappcvgprlemdisj  8011  cauappcvgprlemloc  8012  cauappcvgprlemladdfu  8014  cauappcvgprlemladdfl  8015  cauappcvgprlemladdru  8016  cauappcvgprlem2  8020  caucvgprlemm  8028  caucvgprlemopl  8029  caucvgprlemlol  8030  caucvgprlemopu  8031  caucvgprlemupu  8032  caucvgprlemdisj  8034  caucvgprlemloc  8035  caucvgprlemladdfu  8037  caucvgprlem2  8040  caucvgprprlemell  8045  caucvgprprlemelu  8046  caucvgprprlemml  8054  caucvgprprlemmu  8055  caucvgprprlemexbt  8066  caucvgprprlem2  8070  suplocexprlem2b  8074  suplocexprlemlub  8084  caucvgsr  8162  axcaucvg  8260  infrenegsupex  9976  fseq1p1m1  10482  fz0to4untppr  10512  rebtwn2zlemstep  10668  rebtwn2z  10670  fldiv4p1lem1div2  10721  frec2uzsucd  10819  frec2uzrdg  10827  frecuzrdgsuc  10832  frecuzrdgg  10834  frecuzrdgsuctlem  10841  frecfzennn  10844  0tonninf  10858  1tonninf  10859  seq3val  10878  seqvalcd  10879  seqf1oglem2  10938  facp1  11149  fac2  11150  fac3  11151  fac4  11152  4bc2eq6  11194  fihasheq0  11213  hashprg  11230  hashp1i  11232  pr0hash2ex  11237  hashfzo  11244  hashxp  11248  hashfibc  11264  hashf1lem2  11267  zfz1isolemsplit  11271  hashtpgim  11278  hashtpg  11280  cats1lend  11520  rei  11646  imi  11647  sqrt1  11793  sqrt4  11794  sqrt9  11795  abs0  11805  absi  11806  infxrnegsupex  12010  fsumabs  12213  fsumrelem  12219  hashrabrex  12229  hashuni  12230  isumnn0nn  12241  mertenslem2  12284  ege2le3  12419  efsep  12439  efgt1p2  12443  efgt1p  12444  sin0  12477  cos0  12478  ef01bndlem  12504  cos2bnd  12508  sin4lt0  12515  m1bits  12708  nninfctlemfo  12798  eucalg  12818  prmind2  12879  dfphi2  12979  phiprmpw  12981  phimullem  12984  pockthlem  13116  pockthg  13117  prmunb  13122  ballotfilem1  13201  ballotfilem2  13209  ballotfilemfval0  13216  ballotfilem4  13222  ballotfilemi1  13226  ballotfilemii  13227  ballotfilemic  13231  ballotfilem1c  13232  ballotfilemgun  13249  ballotfilemth  13262  ennnfonelemjn  13274  ennnfonelem1  13279  ennnfonelemhf1o  13285  imasplusg  13609  gsump1  14137  ringidvalg  14242  rmodislmod  14663  lspprid2  14724  sn0cld  15164  txval  15282  hmeontr  15340  comet  15526  cnmetdval  15556  sinhalfpilem  15818  cospi  15827  sincos4thpi  15867  sincos6thpi  15869  sincos3rdpi  15870  sinkpi  15874  reeflog  15890  logfac  15921  logbleb  15989  logblt  15990  sqrt2cxp2logb9e3  16003  lgsval2lem  16046  lgsquadlem2  16114  setsiedg  16210  wlkres  16537  trlreslem  16547  clwwlkccatlem  16558  eupthvdres  16633  eupth2lem3fi  16634  konigsbergvtx  16640  konigsbergiedg  16641  konigsberglem5  16650  konigsberg  16651  ex-ceil  16657  ex-fac  16659  012of  16940  2o01f  16941  nninfsellemqall  16966  nninfomni  16970  nninffeq  16971  isomninnlem  16987  iswomninnlem  17007  ismkvnnlem  17010