Theorem fveq2i 5515

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

Syntax hints:   = wceq 1353   ` cfv 5213

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221

This theorem is referenced by:  fveq12i  5518  ot1stg  6148  ot2ndg  6149  ot3rdgg  6150  algrflem  6225  tfr2a  6317  tfr0dm  6318  tfr0  6319  infisoti  7026  1prl  7549  1pru  7550  ltexprlemell  7592  ltexprlemelu  7593  recexprlemell  7616  recexprlemelu  7617  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemopu  7642  cauappcvgprlemupu  7643  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlem2  7654  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemopu  7665  caucvgprlemupu  7666  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprlem2  7674  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemml  7688  caucvgprprlemmu  7689  caucvgprprlemexbt  7700  caucvgprprlem2  7704  suplocexprlem2b  7708  suplocexprlemlub  7718  caucvgsr  7796  axcaucvg  7894  infrenegsupex  9588  fseq1p1m1  10087  fz0to4untppr  10117  rebtwn2zlemstep  10246  rebtwn2z  10248  fldiv4p1lem1div2  10298  frec2uzsucd  10394  frec2uzrdg  10402  frecuzrdgsuc  10407  frecuzrdgg  10409  frecuzrdgsuctlem  10416  frecfzennn  10419  0tonninf  10432  1tonninf  10433  seq3val  10451  seqvalcd  10452  facp1  10701  fac2  10702  fac3  10703  fac4  10704  4bc2eq6  10745  fihasheq0  10764  hashprg  10779  hashp1i  10781  pr0hash2ex  10786  hashfzo  10793  hashxp  10797  zfz1isolemsplit  10809  rei  10899  imi  10900  sqrt1  11046  sqrt4  11047  sqrt9  11048  abs0  11058  absi  11059  infxrnegsupex  11262  fsumabs  11464  fsumrelem  11470  hashrabrex  11480  hashuni  11481  isumnn0nn  11492  mertenslem2  11535  ege2le3  11670  efsep  11690  efgt1p2  11694  efgt1p  11695  sin0  11728  cos0  11729  ef01bndlem  11755  cos2bnd  11759  sin4lt0  11765  eucalg  12049  prmind2  12110  dfphi2  12210  phiprmpw  12212  phimullem  12215  pockthlem  12344  pockthg  12345  prmunb  12350  ennnfonelemjn  12393  ennnfonelem1  12398  ennnfonelemhf1o  12404  ringidvalg  13044  sn0cld  13419  txval  13537  hmeontr  13595  comet  13781  cnmetdval  13811  sinhalfpilem  13994  cospi  14003  sincos4thpi  14043  sincos6thpi  14045  sincos3rdpi  14046  sinkpi  14050  reeflog  14066  logbleb  14161  logblt  14162  sqrt2cxp2logb9e3  14175  lgsval2lem  14193  ex-ceil  14249  ex-fac  14251  012of  14516  2o01f  14517  nninfsellemqall  14535  nninfomni  14539  nninffeq  14540  isomninnlem  14549  iswomninnlem  14568  ismkvnnlem  14571