Theorem fveq2i 5537

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

Syntax hints:   = wceq 1364  ‘cfv 5235

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243

This theorem is referenced by:  fveq12i  5540  ot1stg  6178  ot2ndg  6179  ot3rdgg  6180  algrflem  6255  tfr2a  6347  tfr0dm  6348  tfr0  6349  infisoti  7062  1prl  7585  1pru  7586  ltexprlemell  7628  ltexprlemelu  7629  recexprlemell  7652  recexprlemelu  7653  cauappcvgprlemm  7675  cauappcvgprlemopl  7676  cauappcvgprlemlol  7677  cauappcvgprlemopu  7678  cauappcvgprlemupu  7679  cauappcvgprlemdisj  7681  cauappcvgprlemloc  7682  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  cauappcvgprlemladdru  7686  cauappcvgprlem2  7690  caucvgprlemm  7698  caucvgprlemopl  7699  caucvgprlemlol  7700  caucvgprlemopu  7701  caucvgprlemupu  7702  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemladdfu  7707  caucvgprlem2  7710  caucvgprprlemell  7715  caucvgprprlemelu  7716  caucvgprprlemml  7724  caucvgprprlemmu  7725  caucvgprprlemexbt  7736  caucvgprprlem2  7740  suplocexprlem2b  7744  suplocexprlemlub  7754  caucvgsr  7832  axcaucvg  7930  infrenegsupex  9626  fseq1p1m1  10126  fz0to4untppr  10156  rebtwn2zlemstep  10285  rebtwn2z  10287  fldiv4p1lem1div2  10338  frec2uzsucd  10434  frec2uzrdg  10442  frecuzrdgsuc  10447  frecuzrdgg  10449  frecuzrdgsuctlem  10456  frecfzennn  10459  0tonninf  10472  1tonninf  10473  seq3val  10491  seqvalcd  10492  facp1  10745  fac2  10746  fac3  10747  fac4  10748  4bc2eq6  10789  fihasheq0  10808  hashprg  10823  hashp1i  10825  pr0hash2ex  10830  hashfzo  10837  hashxp  10841  zfz1isolemsplit  10853  rei  10943  imi  10944  sqrt1  11090  sqrt4  11091  sqrt9  11092  abs0  11102  absi  11103  infxrnegsupex  11306  fsumabs  11508  fsumrelem  11514  hashrabrex  11524  hashuni  11525  isumnn0nn  11536  mertenslem2  11579  ege2le3  11714  efsep  11734  efgt1p2  11738  efgt1p  11739  sin0  11772  cos0  11773  ef01bndlem  11799  cos2bnd  11803  sin4lt0  11809  eucalg  12094  prmind2  12155  dfphi2  12255  phiprmpw  12257  phimullem  12260  pockthlem  12391  pockthg  12392  prmunb  12397  ennnfonelemjn  12456  ennnfonelem1  12461  ennnfonelemhf1o  12467  imasplusg  12788  ringidvalg  13332  rmodislmod  13684  lspprid2  13745  sn0cld  14114  txval  14232  hmeontr  14290  comet  14476  cnmetdval  14506  sinhalfpilem  14689  cospi  14698  sincos4thpi  14738  sincos6thpi  14740  sincos3rdpi  14741  sinkpi  14745  reeflog  14761  logbleb  14856  logblt  14857  sqrt2cxp2logb9e3  14870  lgsval2lem  14889  ex-ceil  14956  ex-fac  14958  012of  15224  2o01f  15225  nninfsellemqall  15243  nninfomni  15247  nninffeq  15248  isomninnlem  15257  iswomninnlem  15276  ismkvnnlem  15279