Theorem fveq2i 5558

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

Syntax hints:   = wceq 1364  ‘cfv 5255

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 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  fveq12i  5561  ot1stg  6207  ot2ndg  6208  ot3rdgg  6209  algrflem  6284  tfr2a  6376  tfr0dm  6377  tfr0  6378  infisoti  7093  1prl  7617  1pru  7618  ltexprlemell  7660  ltexprlemelu  7661  recexprlemell  7684  recexprlemelu  7685  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlem2b  7776  suplocexprlemlub  7786  caucvgsr  7864  axcaucvg  7962  infrenegsupex  9662  fseq1p1m1  10163  fz0to4untppr  10193  rebtwn2zlemstep  10324  rebtwn2z  10326  fldiv4p1lem1div2  10377  frec2uzsucd  10475  frec2uzrdg  10483  frecuzrdgsuc  10488  frecuzrdgg  10490  frecuzrdgsuctlem  10497  frecfzennn  10500  0tonninf  10514  1tonninf  10515  seq3val  10534  seqvalcd  10535  seqf1oglem2  10594  facp1  10804  fac2  10805  fac3  10806  fac4  10807  4bc2eq6  10848  fihasheq0  10867  hashprg  10882  hashp1i  10884  pr0hash2ex  10889  hashfzo  10896  hashxp  10900  zfz1isolemsplit  10912  rei  11046  imi  11047  sqrt1  11193  sqrt4  11194  sqrt9  11195  abs0  11205  absi  11206  infxrnegsupex  11409  fsumabs  11611  fsumrelem  11617  hashrabrex  11627  hashuni  11628  isumnn0nn  11639  mertenslem2  11682  ege2le3  11817  efsep  11837  efgt1p2  11841  efgt1p  11842  sin0  11875  cos0  11876  ef01bndlem  11902  cos2bnd  11906  sin4lt0  11913  nninfctlemfo  12180  eucalg  12200  prmind2  12261  dfphi2  12361  phiprmpw  12363  phimullem  12366  pockthlem  12497  pockthg  12498  prmunb  12503  ennnfonelemjn  12562  ennnfonelem1  12567  ennnfonelemhf1o  12573  imasplusg  12894  ringidvalg  13460  rmodislmod  13850  lspprid2  13911  sn0cld  14316  txval  14434  hmeontr  14492  comet  14678  cnmetdval  14708  sinhalfpilem  14967  cospi  14976  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  sinkpi  15023  reeflog  15039  logbleb  15134  logblt  15135  sqrt2cxp2logb9e3  15148  lgsval2lem  15167  lgsquadlem2  15235  ex-ceil  15288  ex-fac  15290  012of  15556  2o01f  15557  nninfsellemqall  15575  nninfomni  15579  nninffeq  15580  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612