Theorem fveq2i 5701

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

This proof depends on syntax axioms:   = wceq 1402   ` cfv 5380

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq12i  5704  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  algrflem  6469  tfr2a  6596  tfr0dm  6597  tfr0  6598  infisoti  7378  1prl  7928  1pru  7929  ltexprlemell  7971  ltexprlemelu  7972  recexprlemell  7995  recexprlemelu  7996  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlem2b  8087  suplocexprlemlub  8097  caucvgsr  8175  axcaucvg  8273  infrenegsupex  10010  fseq1p1m1  10518  fz0to4untppr  10548  rebtwn2zlemstep  10704  rebtwn2z  10706  fldiv4p1lem1div2  10761  frec2uzsucd  10859  frec2uzrdg  10867  frecuzrdgsuc  10872  frecuzrdgg  10874  frecuzrdgsuctlem  10881  frecfzennn  10884  0tonninf  10898  1tonninf  10899  seq3val  10918  seqvalcd  10919  seqf1oglem2  10978  facp1  11190  fac2  11191  fac3  11192  fac4  11193  4bc2eq6  11235  fihasheq0  11254  hashprg  11271  hashp1i  11273  pr0hash2ex  11278  hashfzo  11285  hashxp  11289  hashfibc  11305  hashf1lem2  11308  zfz1isolemsplit  11312  hashtpgim  11319  hashtpg  11321  cats1lend  11561  rei  11687  imi  11688  sqrt1  11834  sqrt4  11835  sqrt9  11836  abs0  11846  absi  11847  infxrnegsupex  12054  fsumabs  12257  fsumrelem  12263  hashrabrex  12273  hashuni  12274  isumnn0nn  12285  mertenslem2  12328  ege2le3  12463  efsep  12483  efgt1p2  12487  efgt1p  12488  sin0  12521  cos0  12522  ef01bndlem  12548  cos2bnd  12552  sin4lt0  12559  m1bits  12752  nninfctlemfo  12842  eucalg  12862  prmind2  12923  dfphi2  13027  phiprmpw  13029  phimullem  13032  pockthlem  13164  pockthg  13165  prmunb  13170  ballotfilem1  13278  ballotfilem2  13286  ballotfilemfval0  13293  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemgun  13326  ballotfilemth  13339  ennnfonelemjn  13351  ennnfonelem1  13356  ennnfonelemhf1o  13362  imasplusg  13688  gsump1  14247  ringidvalg  14371  rmodislmod  14797  lspprid2  14858  isassa  15111  assamulgscmlem2  15151  sn0cld  15363  txval  15481  hmeontr  15539  comet  15725  cnmetdval  15755  sinhalfpilem  16018  cospi  16027  sincos4thpi  16067  sincos6thpi  16069  sincos3rdpi  16070  sinkpi  16074  reeflog  16092  logfac  16126  logbleb  16197  logblt  16198  sqrt2cxp2logb9e3  16211  birthdaylem2  16226  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  ppi1  16270  ppi1i  16272  ppi2i  16273  cht2  16276  cht3  16277  ppiqub  16293  chtqub  16296  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgsval2lem  16334  lgsquadlem2  16402  setsiedg  16498  wlkres  16825  trlreslem  16835  clwwlkccatlem  16846  eupthvdres  16921  eupth2lem3fi  16922  konigsbergvtx  16928  konigsbergiedg  16929  konigsberglem5  16938  konigsberg  16939  ex-ceil  16945  ex-fac  16947  012of  17228  2o01f  17229  nninfsellemqall  17264  nninfomni  17268  nninffeq  17269  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309