Theorem fveq2i 5557

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

Syntax hints:   = wceq 1364  ‘cfv 5254

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 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  fveq12i  5560  ot1stg  6205  ot2ndg  6206  ot3rdgg  6207  algrflem  6282  tfr2a  6374  tfr0dm  6375  tfr0  6376  infisoti  7091  1prl  7615  1pru  7616  ltexprlemell  7658  ltexprlemelu  7659  recexprlemell  7682  recexprlemelu  7683  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocexprlem2b  7774  suplocexprlemlub  7784  caucvgsr  7862  axcaucvg  7960  infrenegsupex  9659  fseq1p1m1  10160  fz0to4untppr  10190  rebtwn2zlemstep  10321  rebtwn2z  10323  fldiv4p1lem1div2  10374  frec2uzsucd  10472  frec2uzrdg  10480  frecuzrdgsuc  10485  frecuzrdgg  10487  frecuzrdgsuctlem  10494  frecfzennn  10497  0tonninf  10511  1tonninf  10512  seq3val  10531  seqvalcd  10532  seqf1oglem2  10591  facp1  10801  fac2  10802  fac3  10803  fac4  10804  4bc2eq6  10845  fihasheq0  10864  hashprg  10879  hashp1i  10881  pr0hash2ex  10886  hashfzo  10893  hashxp  10897  zfz1isolemsplit  10909  rei  11043  imi  11044  sqrt1  11190  sqrt4  11191  sqrt9  11192  abs0  11202  absi  11203  infxrnegsupex  11406  fsumabs  11608  fsumrelem  11614  hashrabrex  11624  hashuni  11625  isumnn0nn  11636  mertenslem2  11679  ege2le3  11814  efsep  11834  efgt1p2  11838  efgt1p  11839  sin0  11872  cos0  11873  ef01bndlem  11899  cos2bnd  11903  sin4lt0  11910  nninfctlemfo  12177  eucalg  12197  prmind2  12258  dfphi2  12358  phiprmpw  12360  phimullem  12363  pockthlem  12494  pockthg  12495  prmunb  12500  ennnfonelemjn  12559  ennnfonelem1  12564  ennnfonelemhf1o  12570  imasplusg  12891  ringidvalg  13457  rmodislmod  13847  lspprid2  13908  sn0cld  14305  txval  14423  hmeontr  14481  comet  14667  cnmetdval  14697  sinhalfpilem  14926  cospi  14935  sincos4thpi  14975  sincos6thpi  14977  sincos3rdpi  14978  sinkpi  14982  reeflog  14998  logbleb  15093  logblt  15094  sqrt2cxp2logb9e3  15107  lgsval2lem  15126  ex-ceil  15218  ex-fac  15220  012of  15486  2o01f  15487  nninfsellemqall  15505  nninfomni  15509  nninffeq  15510  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542