Theorem fveq2i 5664

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

Syntax hints:   = wceq 1398   ` cfv 5343

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-br 4103  df-iota 5303  df-fv 5351

This theorem is referenced by:  fveq12i  5667  ot1stg  6337  ot2ndg  6338  ot3rdgg  6339  algrflem  6416  tfr2a  6543  tfr0dm  6544  tfr0  6545  infisoti  7314  1prl  7858  1pru  7859  ltexprlemell  7901  ltexprlemelu  7902  recexprlemell  7925  recexprlemelu  7926  cauappcvgprlemm  7948  cauappcvgprlemopl  7949  cauappcvgprlemlol  7950  cauappcvgprlemopu  7951  cauappcvgprlemupu  7952  cauappcvgprlemdisj  7954  cauappcvgprlemloc  7955  cauappcvgprlemladdfu  7957  cauappcvgprlemladdfl  7958  cauappcvgprlemladdru  7959  cauappcvgprlem2  7963  caucvgprlemm  7971  caucvgprlemopl  7972  caucvgprlemlol  7973  caucvgprlemopu  7974  caucvgprlemupu  7975  caucvgprlemdisj  7977  caucvgprlemloc  7978  caucvgprlemladdfu  7980  caucvgprlem2  7983  caucvgprprlemell  7988  caucvgprprlemelu  7989  caucvgprprlemml  7997  caucvgprprlemmu  7998  caucvgprprlemexbt  8009  caucvgprprlem2  8013  suplocexprlem2b  8017  suplocexprlemlub  8027  caucvgsr  8105  axcaucvg  8203  infrenegsupex  9912  fseq1p1m1  10414  fz0to4untppr  10444  rebtwn2zlemstep  10598  rebtwn2z  10600  fldiv4p1lem1div2  10651  frec2uzsucd  10749  frec2uzrdg  10757  frecuzrdgsuc  10762  frecuzrdgg  10764  frecuzrdgsuctlem  10771  frecfzennn  10774  0tonninf  10788  1tonninf  10789  seq3val  10808  seqvalcd  10809  seqf1oglem2  10868  facp1  11078  fac2  11079  fac3  11080  fac4  11081  4bc2eq6  11122  fihasheq0  11141  hashprg  11158  hashp1i  11160  pr0hash2ex  11165  hashfzo  11172  hashxp  11176  zfz1isolemsplit  11188  hashtpgim  11195  hashtpg  11197  cats1lend  11437  rei  11562  imi  11563  sqrt1  11709  sqrt4  11710  sqrt9  11711  abs0  11721  absi  11722  infxrnegsupex  11926  fsumabs  12129  fsumrelem  12135  hashrabrex  12145  hashuni  12146  isumnn0nn  12157  mertenslem2  12200  ege2le3  12335  efsep  12355  efgt1p2  12359  efgt1p  12360  sin0  12393  cos0  12394  ef01bndlem  12420  cos2bnd  12424  sin4lt0  12431  m1bits  12624  nninfctlemfo  12714  eucalg  12734  prmind2  12795  dfphi2  12895  phiprmpw  12897  phimullem  12900  pockthlem  13032  pockthg  13033  prmunb  13038  ennnfonelemjn  13127  ennnfonelem1  13132  ennnfonelemhf1o  13138  imasplusg  13495  ringidvalg  14079  rmodislmod  14471  lspprid2  14532  sn0cld  14972  txval  15090  hmeontr  15148  comet  15334  cnmetdval  15364  sinhalfpilem  15626  cospi  15635  sincos4thpi  15675  sincos6thpi  15677  sincos3rdpi  15678  sinkpi  15682  reeflog  15698  logbleb  15796  logblt  15797  sqrt2cxp2logb9e3  15810  lgsval2lem  15853  lgsquadlem2  15921  setsiedg  16017  wlkres  16344  trlreslem  16354  clwwlkccatlem  16365  eupthvdres  16440  eupth2lem3fi  16441  konigsbergvtx  16447  konigsbergiedg  16448  konigsberglem5  16457  konigsberg  16458  ex-ceil  16464  ex-fac  16466  012of  16737  2o01f  16738  nninfsellemqall  16763  nninfomni  16767  nninffeq  16768  isomninnlem  16784  iswomninnlem  16804  ismkvnnlem  16807  gfsump1  16837