Theorem fveq2i 5675

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

Syntax hints:   = wceq 1398   ` cfv 5354

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362

This theorem is referenced by:  fveq12i  5678  ot1stg  6348  ot2ndg  6349  ot3rdgg  6350  algrflem  6427  tfr2a  6554  tfr0dm  6555  tfr0  6556  infisoti  7325  1prl  7872  1pru  7873  ltexprlemell  7915  ltexprlemelu  7916  recexprlemell  7939  recexprlemelu  7940  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemlol  7964  cauappcvgprlemopu  7965  cauappcvgprlemupu  7966  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  cauappcvgprlem2  7977  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemlol  7987  caucvgprlemopu  7988  caucvgprlemupu  7989  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemladdfu  7994  caucvgprlem2  7997  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemexbt  8023  caucvgprprlem2  8027  suplocexprlem2b  8031  suplocexprlemlub  8041  caucvgsr  8119  axcaucvg  8217  infrenegsupex  9929  fseq1p1m1  10432  fz0to4untppr  10462  rebtwn2zlemstep  10616  rebtwn2z  10618  fldiv4p1lem1div2  10669  frec2uzsucd  10767  frec2uzrdg  10775  frecuzrdgsuc  10780  frecuzrdgg  10782  frecuzrdgsuctlem  10789  frecfzennn  10792  0tonninf  10806  1tonninf  10807  seq3val  10826  seqvalcd  10827  seqf1oglem2  10886  facp1  11096  fac2  11097  fac3  11098  fac4  11099  4bc2eq6  11141  fihasheq0  11160  hashprg  11177  hashp1i  11179  pr0hash2ex  11184  hashfzo  11191  hashxp  11195  hashfibc  11211  zfz1isolemsplit  11214  hashtpgim  11221  hashtpg  11223  cats1lend  11463  rei  11588  imi  11589  sqrt1  11735  sqrt4  11736  sqrt9  11737  abs0  11747  absi  11748  infxrnegsupex  11952  fsumabs  12155  fsumrelem  12161  hashrabrex  12171  hashuni  12172  isumnn0nn  12183  mertenslem2  12226  ege2le3  12361  efsep  12381  efgt1p2  12385  efgt1p  12386  sin0  12419  cos0  12420  ef01bndlem  12446  cos2bnd  12450  sin4lt0  12457  m1bits  12650  nninfctlemfo  12740  eucalg  12760  prmind2  12821  dfphi2  12921  phiprmpw  12923  phimullem  12926  pockthlem  13058  pockthg  13059  prmunb  13064  ballotfilem1  13143  ballotfilem2  13149  ballotfilemfval0  13156  ballotfilem4  13159  ennnfonelemjn  13170  ennnfonelem1  13175  ennnfonelemhf1o  13181  imasplusg  13538  ringidvalg  14122  rmodislmod  14516  lspprid2  14577  sn0cld  15019  txval  15137  hmeontr  15195  comet  15381  cnmetdval  15411  sinhalfpilem  15673  cospi  15682  sincos4thpi  15722  sincos6thpi  15724  sincos3rdpi  15725  sinkpi  15729  reeflog  15745  logbleb  15843  logblt  15844  sqrt2cxp2logb9e3  15857  lgsval2lem  15900  lgsquadlem2  15968  setsiedg  16064  wlkres  16391  trlreslem  16401  clwwlkccatlem  16412  eupthvdres  16487  eupth2lem3fi  16488  konigsbergvtx  16494  konigsbergiedg  16495  konigsberglem5  16504  konigsberg  16505  ex-ceil  16511  ex-fac  16513  012of  16784  2o01f  16785  nninfsellemqall  16810  nninfomni  16814  nninffeq  16815  isomninnlem  16831  iswomninnlem  16851  ismkvnnlem  16854  gfsump1  16885