Theorem fveq2i 5673

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

Syntax hints:   = wceq 1398  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  fveq12i  5676  ot1stg  6346  ot2ndg  6347  ot3rdgg  6348  algrflem  6425  tfr2a  6552  tfr0dm  6553  tfr0  6554  infisoti  7323  1prl  7870  1pru  7871  ltexprlemell  7913  ltexprlemelu  7914  recexprlemell  7937  recexprlemelu  7938  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlem2  7975  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlem2  7995  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemexbt  8021  caucvgprprlem2  8025  suplocexprlem2b  8029  suplocexprlemlub  8039  caucvgsr  8117  axcaucvg  8215  infrenegsupex  9926  fseq1p1m1  10428  fz0to4untppr  10458  rebtwn2zlemstep  10612  rebtwn2z  10614  fldiv4p1lem1div2  10665  frec2uzsucd  10763  frec2uzrdg  10771  frecuzrdgsuc  10776  frecuzrdgg  10778  frecuzrdgsuctlem  10785  frecfzennn  10788  0tonninf  10802  1tonninf  10803  seq3val  10822  seqvalcd  10823  seqf1oglem2  10882  facp1  11092  fac2  11093  fac3  11094  fac4  11095  4bc2eq6  11137  fihasheq0  11156  hashprg  11173  hashp1i  11175  pr0hash2ex  11180  hashfzo  11187  hashxp  11191  hashfibc  11207  zfz1isolemsplit  11210  hashtpgim  11217  hashtpg  11219  cats1lend  11459  rei  11584  imi  11585  sqrt1  11731  sqrt4  11732  sqrt9  11733  abs0  11743  absi  11744  infxrnegsupex  11948  fsumabs  12151  fsumrelem  12157  hashrabrex  12167  hashuni  12168  isumnn0nn  12179  mertenslem2  12222  ege2le3  12357  efsep  12377  efgt1p2  12381  efgt1p  12382  sin0  12415  cos0  12416  ef01bndlem  12442  cos2bnd  12446  sin4lt0  12453  m1bits  12646  nninfctlemfo  12736  eucalg  12756  prmind2  12817  dfphi2  12917  phiprmpw  12919  phimullem  12922  pockthlem  13054  pockthg  13055  prmunb  13060  ballotfilem1  13139  ballotfilem2  13142  ennnfonelemjn  13153  ennnfonelem1  13158  ennnfonelemhf1o  13164  imasplusg  13521  ringidvalg  14105  rmodislmod  14499  lspprid2  14560  sn0cld  15002  txval  15120  hmeontr  15178  comet  15364  cnmetdval  15394  sinhalfpilem  15656  cospi  15665  sincos4thpi  15705  sincos6thpi  15707  sincos3rdpi  15708  sinkpi  15712  reeflog  15728  logbleb  15826  logblt  15827  sqrt2cxp2logb9e3  15840  lgsval2lem  15883  lgsquadlem2  15951  setsiedg  16047  wlkres  16374  trlreslem  16384  clwwlkccatlem  16395  eupthvdres  16470  eupth2lem3fi  16471  konigsbergvtx  16477  konigsbergiedg  16478  konigsberglem5  16487  konigsberg  16488  ex-ceil  16494  ex-fac  16496  012of  16767  2o01f  16768  nninfsellemqall  16793  nninfomni  16797  nninffeq  16798  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837  gfsump1  16868