Theorem fveq2i 5561

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

Syntax hints:   = wceq 1364   ` cfv 5258

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266

This theorem is referenced by:  fveq12i  5564  ot1stg  6210  ot2ndg  6211  ot3rdgg  6212  algrflem  6287  tfr2a  6379  tfr0dm  6380  tfr0  6381  infisoti  7098  1prl  7622  1pru  7623  ltexprlemell  7665  ltexprlemelu  7666  recexprlemell  7689  recexprlemelu  7690  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlem2  7727  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocexprlem2b  7781  suplocexprlemlub  7791  caucvgsr  7869  axcaucvg  7967  infrenegsupex  9668  fseq1p1m1  10169  fz0to4untppr  10199  rebtwn2zlemstep  10342  rebtwn2z  10344  fldiv4p1lem1div2  10395  frec2uzsucd  10493  frec2uzrdg  10501  frecuzrdgsuc  10506  frecuzrdgg  10508  frecuzrdgsuctlem  10515  frecfzennn  10518  0tonninf  10532  1tonninf  10533  seq3val  10552  seqvalcd  10553  seqf1oglem2  10612  facp1  10822  fac2  10823  fac3  10824  fac4  10825  4bc2eq6  10866  fihasheq0  10885  hashprg  10900  hashp1i  10902  pr0hash2ex  10907  hashfzo  10914  hashxp  10918  zfz1isolemsplit  10930  rei  11064  imi  11065  sqrt1  11211  sqrt4  11212  sqrt9  11213  abs0  11223  absi  11224  infxrnegsupex  11428  fsumabs  11630  fsumrelem  11636  hashrabrex  11646  hashuni  11647  isumnn0nn  11658  mertenslem2  11701  ege2le3  11836  efsep  11856  efgt1p2  11860  efgt1p  11861  sin0  11894  cos0  11895  ef01bndlem  11921  cos2bnd  11925  sin4lt0  11932  nninfctlemfo  12207  eucalg  12227  prmind2  12288  dfphi2  12388  phiprmpw  12390  phimullem  12393  pockthlem  12525  pockthg  12526  prmunb  12531  ennnfonelemjn  12619  ennnfonelem1  12624  ennnfonelemhf1o  12630  imasplusg  12951  ringidvalg  13517  rmodislmod  13907  lspprid2  13968  sn0cld  14373  txval  14491  hmeontr  14549  comet  14735  cnmetdval  14765  sinhalfpilem  15027  cospi  15036  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  sinkpi  15083  reeflog  15099  logbleb  15197  logblt  15198  sqrt2cxp2logb9e3  15211  lgsval2lem  15251  lgsquadlem2  15319  ex-ceil  15372  ex-fac  15374  012of  15640  2o01f  15641  nninfsellemqall  15659  nninfomni  15663  nninffeq  15664  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696