Theorem fveq2i 5464

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 5461	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1332  ‘cfv 5163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-rex 2438  df-v 2711  df-un 3102  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-iota 5128  df-fv 5171

This theorem is referenced by:  fveq12i  5467  ot1stg  6090  ot2ndg  6091  ot3rdgg  6092  algrflem  6166  tfr2a  6258  tfr0dm  6259  tfr0  6260  infisoti  6964  1prl  7454  1pru  7455  ltexprlemell  7497  ltexprlemelu  7498  recexprlemell  7521  recexprlemelu  7522  cauappcvgprlemm  7544  cauappcvgprlemopl  7545  cauappcvgprlemlol  7546  cauappcvgprlemopu  7547  cauappcvgprlemupu  7548  cauappcvgprlemdisj  7550  cauappcvgprlemloc  7551  cauappcvgprlemladdfu  7553  cauappcvgprlemladdfl  7554  cauappcvgprlemladdru  7555  cauappcvgprlem2  7559  caucvgprlemm  7567  caucvgprlemopl  7568  caucvgprlemlol  7569  caucvgprlemopu  7570  caucvgprlemupu  7571  caucvgprlemdisj  7573  caucvgprlemloc  7574  caucvgprlemladdfu  7576  caucvgprlem2  7579  caucvgprprlemell  7584  caucvgprprlemelu  7585  caucvgprprlemml  7593  caucvgprprlemmu  7594  caucvgprprlemexbt  7605  caucvgprprlem2  7609  suplocexprlem2b  7613  suplocexprlemlub  7623  caucvgsr  7701  axcaucvg  7799  infrenegsupex  9484  fseq1p1m1  9974  rebtwn2zlemstep  10130  rebtwn2z  10132  fldiv4p1lem1div2  10182  frec2uzsucd  10278  frec2uzrdg  10286  frecuzrdgsuc  10291  frecuzrdgg  10293  frecuzrdgsuctlem  10300  frecfzennn  10303  0tonninf  10316  1tonninf  10317  seq3val  10335  seqvalcd  10336  facp1  10581  fac2  10582  fac3  10583  fac4  10584  4bc2eq6  10625  fihasheq0  10645  hashprg  10659  hashp1i  10661  pr0hash2ex  10666  hashfzo  10673  hashxp  10677  zfz1isolemsplit  10686  rei  10776  imi  10777  sqrt1  10923  sqrt4  10924  sqrt9  10925  abs0  10935  absi  10936  infxrnegsupex  11137  fsumabs  11339  fsumrelem  11345  hashrabrex  11355  hashuni  11356  isumnn0nn  11367  mertenslem2  11410  ege2le3  11545  efsep  11565  efgt1p2  11569  efgt1p  11570  sin0  11603  cos0  11604  ef01bndlem  11630  cos2bnd  11634  sin4lt0  11640  eucalg  11907  prmind2  11968  dfphi2  12063  phiprmpw  12065  phimullem  12068  ennnfonelemjn  12082  ennnfonelem1  12087  ennnfonelemhf1o  12093  sn0cld  12476  txval  12594  hmeontr  12652  comet  12838  cnmetdval  12868  sinhalfpilem  13051  cospi  13060  sincos4thpi  13100  sincos6thpi  13102  sincos3rdpi  13103  sinkpi  13107  reeflog  13123  logbleb  13217  logblt  13218  sqrt2cxp2logb9e3  13231  ex-ceil  13240  ex-fac  13242  012of  13506  2o01f  13507  nninfsellemqall  13528  nninfomni  13532  nninffeq  13533  isomninnlem  13542  iswomninnlem  13561  ismkvnnlem  13564