Theorem fveq2i 5519

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

Syntax hints:   = wceq 1353   ` cfv 5217

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  fveq12i  5522  ot1stg  6153  ot2ndg  6154  ot3rdgg  6155  algrflem  6230  tfr2a  6322  tfr0dm  6323  tfr0  6324  infisoti  7031  1prl  7554  1pru  7555  ltexprlemell  7597  ltexprlemelu  7598  recexprlemell  7621  recexprlemelu  7622  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlem2  7659  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprlem2  7679  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemexbt  7705  caucvgprprlem2  7709  suplocexprlem2b  7713  suplocexprlemlub  7723  caucvgsr  7801  axcaucvg  7899  infrenegsupex  9594  fseq1p1m1  10094  fz0to4untppr  10124  rebtwn2zlemstep  10253  rebtwn2z  10255  fldiv4p1lem1div2  10305  frec2uzsucd  10401  frec2uzrdg  10409  frecuzrdgsuc  10414  frecuzrdgg  10416  frecuzrdgsuctlem  10423  frecfzennn  10426  0tonninf  10439  1tonninf  10440  seq3val  10458  seqvalcd  10459  facp1  10710  fac2  10711  fac3  10712  fac4  10713  4bc2eq6  10754  fihasheq0  10773  hashprg  10788  hashp1i  10790  pr0hash2ex  10795  hashfzo  10802  hashxp  10806  zfz1isolemsplit  10818  rei  10908  imi  10909  sqrt1  11055  sqrt4  11056  sqrt9  11057  abs0  11067  absi  11068  infxrnegsupex  11271  fsumabs  11473  fsumrelem  11479  hashrabrex  11489  hashuni  11490  isumnn0nn  11501  mertenslem2  11544  ege2le3  11679  efsep  11699  efgt1p2  11703  efgt1p  11704  sin0  11737  cos0  11738  ef01bndlem  11764  cos2bnd  11768  sin4lt0  11774  eucalg  12059  prmind2  12120  dfphi2  12220  phiprmpw  12222  phimullem  12225  pockthlem  12354  pockthg  12355  prmunb  12360  ennnfonelemjn  12403  ennnfonelem1  12408  ennnfonelemhf1o  12414  imasplusg  12729  ringidvalg  13144  rmodislmod  13441  sn0cld  13640  txval  13758  hmeontr  13816  comet  14002  cnmetdval  14032  sinhalfpilem  14215  cospi  14224  sincos4thpi  14264  sincos6thpi  14266  sincos3rdpi  14267  sinkpi  14271  reeflog  14287  logbleb  14382  logblt  14383  sqrt2cxp2logb9e3  14396  lgsval2lem  14414  ex-ceil  14481  ex-fac  14483  012of  14748  2o01f  14749  nninfsellemqall  14767  nninfomni  14771  nninffeq  14772  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803