Theorem fveq2i 5432

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

Syntax hints:   = wceq 1332  ‘cfv 5131

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 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139

This theorem is referenced by:  fveq12i  5435  ot1stg  6058  ot2ndg  6059  ot3rdgg  6060  algrflem  6134  tfr2a  6226  tfr0dm  6227  tfr0  6228  infisoti  6927  1prl  7387  1pru  7388  ltexprlemell  7430  ltexprlemelu  7431  recexprlemell  7454  recexprlemelu  7455  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocexprlem2b  7546  suplocexprlemlub  7556  caucvgsr  7634  axcaucvg  7732  infrenegsupex  9416  fseq1p1m1  9905  rebtwn2zlemstep  10061  rebtwn2z  10063  fldiv4p1lem1div2  10109  frec2uzsucd  10205  frec2uzrdg  10213  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdgsuctlem  10227  frecfzennn  10230  0tonninf  10243  1tonninf  10244  seq3val  10262  seqvalcd  10263  facp1  10508  fac2  10509  fac3  10510  fac4  10511  4bc2eq6  10552  fihasheq0  10572  hashprg  10586  hashp1i  10588  pr0hash2ex  10593  hashfzo  10600  hashxp  10604  zfz1isolemsplit  10613  rei  10703  imi  10704  sqrt1  10850  sqrt4  10851  sqrt9  10852  abs0  10862  absi  10863  infxrnegsupex  11064  fsumabs  11266  fsumrelem  11272  hashrabrex  11282  hashuni  11283  isumnn0nn  11294  mertenslem2  11337  ege2le3  11414  efsep  11434  efgt1p2  11438  efgt1p  11439  sin0  11472  cos0  11473  ef01bndlem  11499  cos2bnd  11503  sin4lt0  11509  eucalg  11776  prmind2  11837  dfphi2  11932  phiprmpw  11934  phimullem  11937  ennnfonelemjn  11951  ennnfonelem1  11956  ennnfonelemhf1o  11962  sn0cld  12345  txval  12463  hmeontr  12521  comet  12707  cnmetdval  12737  sinhalfpilem  12920  cospi  12929  sincos4thpi  12969  sincos6thpi  12971  sincos3rdpi  12972  sinkpi  12976  reeflog  12992  logbleb  13086  logblt  13087  sqrt2cxp2logb9e3  13100  ex-ceil  13109  ex-fac  13111  012of  13363  2o01f  13364  nninfsellemqall  13386  nninfomni  13390  nninffeq  13391  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419