Theorem fveq2i 5532

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

Syntax hints:   = wceq 1363   ` cfv 5230

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-rex 2473  df-v 2753  df-un 3147  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-br 4018  df-iota 5192  df-fv 5238

This theorem is referenced by:  fveq12i  5535  ot1stg  6170  ot2ndg  6171  ot3rdgg  6172  algrflem  6247  tfr2a  6339  tfr0dm  6340  tfr0  6341  infisoti  7048  1prl  7571  1pru  7572  ltexprlemell  7614  ltexprlemelu  7615  recexprlemell  7638  recexprlemelu  7639  cauappcvgprlemm  7661  cauappcvgprlemopl  7662  cauappcvgprlemlol  7663  cauappcvgprlemopu  7664  cauappcvgprlemupu  7665  cauappcvgprlemdisj  7667  cauappcvgprlemloc  7668  cauappcvgprlemladdfu  7670  cauappcvgprlemladdfl  7671  cauappcvgprlemladdru  7672  cauappcvgprlem2  7676  caucvgprlemm  7684  caucvgprlemopl  7685  caucvgprlemlol  7686  caucvgprlemopu  7687  caucvgprlemupu  7688  caucvgprlemdisj  7690  caucvgprlemloc  7691  caucvgprlemladdfu  7693  caucvgprlem2  7696  caucvgprprlemell  7701  caucvgprprlemelu  7702  caucvgprprlemml  7710  caucvgprprlemmu  7711  caucvgprprlemexbt  7722  caucvgprprlem2  7726  suplocexprlem2b  7730  suplocexprlemlub  7740  caucvgsr  7818  axcaucvg  7916  infrenegsupex  9611  fseq1p1m1  10111  fz0to4untppr  10141  rebtwn2zlemstep  10270  rebtwn2z  10272  fldiv4p1lem1div2  10322  frec2uzsucd  10418  frec2uzrdg  10426  frecuzrdgsuc  10431  frecuzrdgg  10433  frecuzrdgsuctlem  10440  frecfzennn  10443  0tonninf  10456  1tonninf  10457  seq3val  10475  seqvalcd  10476  facp1  10727  fac2  10728  fac3  10729  fac4  10730  4bc2eq6  10771  fihasheq0  10790  hashprg  10805  hashp1i  10807  pr0hash2ex  10812  hashfzo  10819  hashxp  10823  zfz1isolemsplit  10835  rei  10925  imi  10926  sqrt1  11072  sqrt4  11073  sqrt9  11074  abs0  11084  absi  11085  infxrnegsupex  11288  fsumabs  11490  fsumrelem  11496  hashrabrex  11506  hashuni  11507  isumnn0nn  11518  mertenslem2  11561  ege2le3  11696  efsep  11716  efgt1p2  11720  efgt1p  11721  sin0  11754  cos0  11755  ef01bndlem  11781  cos2bnd  11785  sin4lt0  11791  eucalg  12076  prmind2  12137  dfphi2  12237  phiprmpw  12239  phimullem  12242  pockthlem  12371  pockthg  12372  prmunb  12377  ennnfonelemjn  12420  ennnfonelem1  12425  ennnfonelemhf1o  12431  imasplusg  12750  ringidvalg  13275  rmodislmod  13627  lspprid2  13688  sn0cld  14020  txval  14138  hmeontr  14196  comet  14382  cnmetdval  14412  sinhalfpilem  14595  cospi  14604  sincos4thpi  14644  sincos6thpi  14646  sincos3rdpi  14647  sinkpi  14651  reeflog  14667  logbleb  14762  logblt  14763  sqrt2cxp2logb9e3  14776  lgsval2lem  14794  ex-ceil  14861  ex-fac  14863  012of  15129  2o01f  15130  nninfsellemqall  15148  nninfomni  15152  nninffeq  15153  isomninnlem  15162  iswomninnlem  15181  ismkvnnlem  15184