Theorem fveq2i 5518

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

Syntax hints:   = wceq 1353   ` cfv 5216

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 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  fveq12i  5521  ot1stg  6152  ot2ndg  6153  ot3rdgg  6154  algrflem  6229  tfr2a  6321  tfr0dm  6322  tfr0  6323  infisoti  7030  1prl  7553  1pru  7554  ltexprlemell  7596  ltexprlemelu  7597  recexprlemell  7620  recexprlemelu  7621  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemexbt  7704  caucvgprprlem2  7708  suplocexprlem2b  7712  suplocexprlemlub  7722  caucvgsr  7800  axcaucvg  7898  infrenegsupex  9593  fseq1p1m1  10093  fz0to4untppr  10123  rebtwn2zlemstep  10252  rebtwn2z  10254  fldiv4p1lem1div2  10304  frec2uzsucd  10400  frec2uzrdg  10408  frecuzrdgsuc  10413  frecuzrdgg  10415  frecuzrdgsuctlem  10422  frecfzennn  10425  0tonninf  10438  1tonninf  10439  seq3val  10457  seqvalcd  10458  facp1  10709  fac2  10710  fac3  10711  fac4  10712  4bc2eq6  10753  fihasheq0  10772  hashprg  10787  hashp1i  10789  pr0hash2ex  10794  hashfzo  10801  hashxp  10805  zfz1isolemsplit  10817  rei  10907  imi  10908  sqrt1  11054  sqrt4  11055  sqrt9  11056  abs0  11066  absi  11067  infxrnegsupex  11270  fsumabs  11472  fsumrelem  11478  hashrabrex  11488  hashuni  11489  isumnn0nn  11500  mertenslem2  11543  ege2le3  11678  efsep  11698  efgt1p2  11702  efgt1p  11703  sin0  11736  cos0  11737  ef01bndlem  11763  cos2bnd  11767  sin4lt0  11773  eucalg  12058  prmind2  12119  dfphi2  12219  phiprmpw  12221  phimullem  12224  pockthlem  12353  pockthg  12354  prmunb  12359  ennnfonelemjn  12402  ennnfonelem1  12407  ennnfonelemhf1o  12413  imasplusg  12728  ringidvalg  13142  sn0cld  13607  txval  13725  hmeontr  13783  comet  13969  cnmetdval  13999  sinhalfpilem  14182  cospi  14191  sincos4thpi  14231  sincos6thpi  14233  sincos3rdpi  14234  sinkpi  14238  reeflog  14254  logbleb  14349  logblt  14350  sqrt2cxp2logb9e3  14363  lgsval2lem  14381  ex-ceil  14448  ex-fac  14450  012of  14715  2o01f  14716  nninfsellemqall  14734  nninfomni  14738  nninffeq  14739  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770