Theorem fveq2i 5602

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

Syntax hints:   = wceq 1373   ` cfv 5290

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  fveq12i  5605  ot1stg  6261  ot2ndg  6262  ot3rdgg  6263  algrflem  6338  tfr2a  6430  tfr0dm  6431  tfr0  6432  infisoti  7160  1prl  7703  1pru  7704  ltexprlemell  7746  ltexprlemelu  7747  recexprlemell  7770  recexprlemelu  7771  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlem2  7828  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemexbt  7854  caucvgprprlem2  7858  suplocexprlem2b  7862  suplocexprlemlub  7872  caucvgsr  7950  axcaucvg  8048  infrenegsupex  9750  fseq1p1m1  10251  fz0to4untppr  10281  rebtwn2zlemstep  10432  rebtwn2z  10434  fldiv4p1lem1div2  10485  frec2uzsucd  10583  frec2uzrdg  10591  frecuzrdgsuc  10596  frecuzrdgg  10598  frecuzrdgsuctlem  10605  frecfzennn  10608  0tonninf  10622  1tonninf  10623  seq3val  10642  seqvalcd  10643  seqf1oglem2  10702  facp1  10912  fac2  10913  fac3  10914  fac4  10915  4bc2eq6  10956  fihasheq0  10975  hashprg  10990  hashp1i  10992  pr0hash2ex  10997  hashfzo  11004  hashxp  11008  zfz1isolemsplit  11020  rei  11325  imi  11326  sqrt1  11472  sqrt4  11473  sqrt9  11474  abs0  11484  absi  11485  infxrnegsupex  11689  fsumabs  11891  fsumrelem  11897  hashrabrex  11907  hashuni  11908  isumnn0nn  11919  mertenslem2  11962  ege2le3  12097  efsep  12117  efgt1p2  12121  efgt1p  12122  sin0  12155  cos0  12156  ef01bndlem  12182  cos2bnd  12186  sin4lt0  12193  m1bits  12386  nninfctlemfo  12476  eucalg  12496  prmind2  12557  dfphi2  12657  phiprmpw  12659  phimullem  12662  pockthlem  12794  pockthg  12795  prmunb  12800  ennnfonelemjn  12888  ennnfonelem1  12893  ennnfonelemhf1o  12899  imasplusg  13255  ringidvalg  13838  rmodislmod  14228  lspprid2  14289  sn0cld  14724  txval  14842  hmeontr  14900  comet  15086  cnmetdval  15116  sinhalfpilem  15378  cospi  15387  sincos4thpi  15427  sincos6thpi  15429  sincos3rdpi  15430  sinkpi  15434  reeflog  15450  logbleb  15548  logblt  15549  sqrt2cxp2logb9e3  15562  lgsval2lem  15602  lgsquadlem2  15670  ex-ceil  15862  ex-fac  15864  012of  16130  2o01f  16131  nninfsellemqall  16154  nninfomni  16158  nninffeq  16159  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193