Theorem fveq2i 5693

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

Syntax hints:   = wceq 1402  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  fveq12i  5696  ot1stg  6376  ot2ndg  6377  ot3rdgg  6378  algrflem  6455  tfr2a  6582  tfr0dm  6583  tfr0  6584  infisoti  7362  1prl  7912  1pru  7913  ltexprlemell  7955  ltexprlemelu  7956  recexprlemell  7979  recexprlemelu  7980  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocexprlem2b  8071  suplocexprlemlub  8081  caucvgsr  8159  axcaucvg  8257  infrenegsupex  9973  fseq1p1m1  10479  fz0to4untppr  10509  rebtwn2zlemstep  10665  rebtwn2z  10667  fldiv4p1lem1div2  10718  frec2uzsucd  10816  frec2uzrdg  10824  frecuzrdgsuc  10829  frecuzrdgg  10831  frecuzrdgsuctlem  10838  frecfzennn  10841  0tonninf  10855  1tonninf  10856  seq3val  10875  seqvalcd  10876  seqf1oglem2  10935  facp1  11146  fac2  11147  fac3  11148  fac4  11149  4bc2eq6  11191  fihasheq0  11210  hashprg  11227  hashp1i  11229  pr0hash2ex  11234  hashfzo  11241  hashxp  11245  hashfibc  11261  hashf1lem2  11264  zfz1isolemsplit  11268  hashtpgim  11275  hashtpg  11277  cats1lend  11517  rei  11643  imi  11644  sqrt1  11790  sqrt4  11791  sqrt9  11792  abs0  11802  absi  11803  infxrnegsupex  12007  fsumabs  12210  fsumrelem  12216  hashrabrex  12226  hashuni  12227  isumnn0nn  12238  mertenslem2  12281  ege2le3  12416  efsep  12436  efgt1p2  12440  efgt1p  12441  sin0  12474  cos0  12475  ef01bndlem  12501  cos2bnd  12505  sin4lt0  12512  m1bits  12705  nninfctlemfo  12795  eucalg  12815  prmind2  12876  dfphi2  12976  phiprmpw  12978  phimullem  12981  pockthlem  13113  pockthg  13114  prmunb  13119  ballotfilem1  13198  ballotfilem2  13206  ballotfilemfval0  13213  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemgun  13246  ballotfilemth  13259  ennnfonelemjn  13271  ennnfonelem1  13276  ennnfonelemhf1o  13282  imasplusg  13606  gsump1  14134  ringidvalg  14239  rmodislmod  14660  lspprid2  14721  sn0cld  15161  txval  15279  hmeontr  15337  comet  15523  cnmetdval  15553  sinhalfpilem  15815  cospi  15824  sincos4thpi  15864  sincos6thpi  15866  sincos3rdpi  15867  sinkpi  15871  reeflog  15887  logfac  15918  logbleb  15986  logblt  15987  sqrt2cxp2logb9e3  16000  lgsval2lem  16043  lgsquadlem2  16111  setsiedg  16207  wlkres  16534  trlreslem  16544  clwwlkccatlem  16555  eupthvdres  16630  eupth2lem3fi  16631  konigsbergvtx  16637  konigsbergiedg  16638  konigsberglem5  16647  konigsberg  16648  ex-ceil  16654  ex-fac  16656  012of  16937  2o01f  16938  nninfsellemqall  16963  nninfomni  16967  nninffeq  16968  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007