Theorem fveq2i 5581

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

Syntax hints:   = wceq 1373   ` cfv 5272

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  fveq12i  5584  ot1stg  6240  ot2ndg  6241  ot3rdgg  6242  algrflem  6317  tfr2a  6409  tfr0dm  6410  tfr0  6411  infisoti  7136  1prl  7670  1pru  7671  ltexprlemell  7713  ltexprlemelu  7714  recexprlemell  7737  recexprlemelu  7738  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemopu  7763  cauappcvgprlemupu  7764  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlem2  7775  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemopu  7786  caucvgprlemupu  7787  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemladdfu  7792  caucvgprlem2  7795  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemexbt  7821  caucvgprprlem2  7825  suplocexprlem2b  7829  suplocexprlemlub  7839  caucvgsr  7917  axcaucvg  8015  infrenegsupex  9717  fseq1p1m1  10218  fz0to4untppr  10248  rebtwn2zlemstep  10397  rebtwn2z  10399  fldiv4p1lem1div2  10450  frec2uzsucd  10548  frec2uzrdg  10556  frecuzrdgsuc  10561  frecuzrdgg  10563  frecuzrdgsuctlem  10570  frecfzennn  10573  0tonninf  10587  1tonninf  10588  seq3val  10607  seqvalcd  10608  seqf1oglem2  10667  facp1  10877  fac2  10878  fac3  10879  fac4  10880  4bc2eq6  10921  fihasheq0  10940  hashprg  10955  hashp1i  10957  pr0hash2ex  10962  hashfzo  10969  hashxp  10973  zfz1isolemsplit  10985  rei  11243  imi  11244  sqrt1  11390  sqrt4  11391  sqrt9  11392  abs0  11402  absi  11403  infxrnegsupex  11607  fsumabs  11809  fsumrelem  11815  hashrabrex  11825  hashuni  11826  isumnn0nn  11837  mertenslem2  11880  ege2le3  12015  efsep  12035  efgt1p2  12039  efgt1p  12040  sin0  12073  cos0  12074  ef01bndlem  12100  cos2bnd  12104  sin4lt0  12111  m1bits  12304  nninfctlemfo  12394  eucalg  12414  prmind2  12475  dfphi2  12575  phiprmpw  12577  phimullem  12580  pockthlem  12712  pockthg  12713  prmunb  12718  ennnfonelemjn  12806  ennnfonelem1  12811  ennnfonelemhf1o  12817  imasplusg  13173  ringidvalg  13756  rmodislmod  14146  lspprid2  14207  sn0cld  14642  txval  14760  hmeontr  14818  comet  15004  cnmetdval  15034  sinhalfpilem  15296  cospi  15305  sincos4thpi  15345  sincos6thpi  15347  sincos3rdpi  15348  sinkpi  15352  reeflog  15368  logbleb  15466  logblt  15467  sqrt2cxp2logb9e3  15480  lgsval2lem  15520  lgsquadlem2  15588  ex-ceil  15699  ex-fac  15701  012of  15967  2o01f  15968  nninfsellemqall  15989  nninfomni  15993  nninffeq  15994  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028