Theorem fveq2i 5516

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

Syntax hints:   = wceq 1353   ` cfv 5214

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 3810  df-br 4003  df-iota 5176  df-fv 5222

This theorem is referenced by:  fveq12i  5519  ot1stg  6149  ot2ndg  6150  ot3rdgg  6151  algrflem  6226  tfr2a  6318  tfr0dm  6319  tfr0  6320  infisoti  7027  1prl  7550  1pru  7551  ltexprlemell  7593  ltexprlemelu  7594  recexprlemell  7617  recexprlemelu  7618  cauappcvgprlemm  7640  cauappcvgprlemopl  7641  cauappcvgprlemlol  7642  cauappcvgprlemopu  7643  cauappcvgprlemupu  7644  cauappcvgprlemdisj  7646  cauappcvgprlemloc  7647  cauappcvgprlemladdfu  7649  cauappcvgprlemladdfl  7650  cauappcvgprlemladdru  7651  cauappcvgprlem2  7655  caucvgprlemm  7663  caucvgprlemopl  7664  caucvgprlemlol  7665  caucvgprlemopu  7666  caucvgprlemupu  7667  caucvgprlemdisj  7669  caucvgprlemloc  7670  caucvgprlemladdfu  7672  caucvgprlem2  7675  caucvgprprlemell  7680  caucvgprprlemelu  7681  caucvgprprlemml  7689  caucvgprprlemmu  7690  caucvgprprlemexbt  7701  caucvgprprlem2  7705  suplocexprlem2b  7709  suplocexprlemlub  7719  caucvgsr  7797  axcaucvg  7895  infrenegsupex  9589  fseq1p1m1  10088  fz0to4untppr  10118  rebtwn2zlemstep  10247  rebtwn2z  10249  fldiv4p1lem1div2  10299  frec2uzsucd  10395  frec2uzrdg  10403  frecuzrdgsuc  10408  frecuzrdgg  10410  frecuzrdgsuctlem  10417  frecfzennn  10420  0tonninf  10433  1tonninf  10434  seq3val  10452  seqvalcd  10453  facp1  10702  fac2  10703  fac3  10704  fac4  10705  4bc2eq6  10746  fihasheq0  10765  hashprg  10780  hashp1i  10782  pr0hash2ex  10787  hashfzo  10794  hashxp  10798  zfz1isolemsplit  10810  rei  10900  imi  10901  sqrt1  11047  sqrt4  11048  sqrt9  11049  abs0  11059  absi  11060  infxrnegsupex  11263  fsumabs  11465  fsumrelem  11471  hashrabrex  11481  hashuni  11482  isumnn0nn  11493  mertenslem2  11536  ege2le3  11671  efsep  11691  efgt1p2  11695  efgt1p  11696  sin0  11729  cos0  11730  ef01bndlem  11756  cos2bnd  11760  sin4lt0  11766  eucalg  12050  prmind2  12111  dfphi2  12211  phiprmpw  12213  phimullem  12216  pockthlem  12345  pockthg  12346  prmunb  12351  ennnfonelemjn  12394  ennnfonelem1  12399  ennnfonelemhf1o  12405  ringidvalg  13066  sn0cld  13499  txval  13617  hmeontr  13675  comet  13861  cnmetdval  13891  sinhalfpilem  14074  cospi  14083  sincos4thpi  14123  sincos6thpi  14125  sincos3rdpi  14126  sinkpi  14130  reeflog  14146  logbleb  14241  logblt  14242  sqrt2cxp2logb9e3  14255  lgsval2lem  14273  ex-ceil  14329  ex-fac  14331  012of  14596  2o01f  14597  nninfsellemqall  14615  nninfomni  14619  nninffeq  14620  isomninnlem  14629  iswomninnlem  14648  ismkvnnlem  14651