Theorem fveq2i 5579

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fveq2i	⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fveq2 5576	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1373  ‘cfv 5271

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  fveq12i  5582  ot1stg  6238  ot2ndg  6239  ot3rdgg  6240  algrflem  6315  tfr2a  6407  tfr0dm  6408  tfr0  6409  infisoti  7134  1prl  7668  1pru  7669  ltexprlemell  7711  ltexprlemelu  7712  recexprlemell  7735  recexprlemelu  7736  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlem2  7773  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprlem2  7793  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemexbt  7819  caucvgprprlem2  7823  suplocexprlem2b  7827  suplocexprlemlub  7837  caucvgsr  7915  axcaucvg  8013  infrenegsupex  9715  fseq1p1m1  10216  fz0to4untppr  10246  rebtwn2zlemstep  10395  rebtwn2z  10397  fldiv4p1lem1div2  10448  frec2uzsucd  10546  frec2uzrdg  10554  frecuzrdgsuc  10559  frecuzrdgg  10561  frecuzrdgsuctlem  10568  frecfzennn  10571  0tonninf  10585  1tonninf  10586  seq3val  10605  seqvalcd  10606  seqf1oglem2  10665  facp1  10875  fac2  10876  fac3  10877  fac4  10878  4bc2eq6  10919  fihasheq0  10938  hashprg  10953  hashp1i  10955  pr0hash2ex  10960  hashfzo  10967  hashxp  10971  zfz1isolemsplit  10983  rei  11210  imi  11211  sqrt1  11357  sqrt4  11358  sqrt9  11359  abs0  11369  absi  11370  infxrnegsupex  11574  fsumabs  11776  fsumrelem  11782  hashrabrex  11792  hashuni  11793  isumnn0nn  11804  mertenslem2  11847  ege2le3  11982  efsep  12002  efgt1p2  12006  efgt1p  12007  sin0  12040  cos0  12041  ef01bndlem  12067  cos2bnd  12071  sin4lt0  12078  m1bits  12271  nninfctlemfo  12361  eucalg  12381  prmind2  12442  dfphi2  12542  phiprmpw  12544  phimullem  12547  pockthlem  12679  pockthg  12680  prmunb  12685  ennnfonelemjn  12773  ennnfonelem1  12778  ennnfonelemhf1o  12784  imasplusg  13140  ringidvalg  13723  rmodislmod  14113  lspprid2  14174  sn0cld  14609  txval  14727  hmeontr  14785  comet  14971  cnmetdval  15001  sinhalfpilem  15263  cospi  15272  sincos4thpi  15312  sincos6thpi  15314  sincos3rdpi  15315  sinkpi  15319  reeflog  15335  logbleb  15433  logblt  15434  sqrt2cxp2logb9e3  15447  lgsval2lem  15487  lgsquadlem2  15555  ex-ceil  15662  ex-fac  15664  012of  15930  2o01f  15931  nninfsellemqall  15952  nninfomni  15956  nninffeq  15957  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991