Theorem fveq2i 5701

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

This proof depends on syntax axioms:   = wceq 1402  ‘cfv 5380

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq12i  5704  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  algrflem  6469  tfr2a  6597  tfr0dm  6598  tfr0  6599  infisoti  7378  1prl  7928  1pru  7929  ltexprlemell  7971  ltexprlemelu  7972  recexprlemell  7995  recexprlemelu  7996  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlem2b  8087  suplocexprlemlub  8097  caucvgsr  8175  axcaucvg  8273  infrenegsupex  10009  fseq1p1m1  10517  fz0to4untppr  10547  rebtwn2zlemstep  10703  rebtwn2z  10705  fldiv4p1lem1div2  10760  frec2uzsucd  10858  frec2uzrdg  10866  frecuzrdgsuc  10871  frecuzrdgg  10873  frecuzrdgsuctlem  10880  frecfzennn  10883  0tonninf  10897  1tonninf  10898  seq3val  10917  seqvalcd  10918  seqf1oglem2  10977  facp1  11189  fac2  11190  fac3  11191  fac4  11192  4bc2eq6  11234  fihasheq0  11253  hashprg  11270  hashp1i  11272  pr0hash2ex  11277  hashfzo  11284  hashxp  11288  hashfibc  11304  hashf1lem2  11307  zfz1isolemsplit  11311  hashtpgim  11318  hashtpg  11320  cats1lend  11560  rei  11686  imi  11687  sqrt1  11833  sqrt4  11834  sqrt9  11835  abs0  11845  absi  11846  infxrnegsupex  12053  fsumabs  12256  fsumrelem  12262  hashrabrex  12272  hashuni  12273  isumnn0nn  12284  mertenslem2  12327  ege2le3  12462  efsep  12482  efgt1p2  12486  efgt1p  12487  sin0  12520  cos0  12521  ef01bndlem  12547  cos2bnd  12551  sin4lt0  12558  m1bits  12751  nninfctlemfo  12841  eucalg  12861  prmind2  12922  dfphi2  13026  phiprmpw  13028  phimullem  13031  pockthlem  13163  pockthg  13164  prmunb  13169  ballotfilem1  13277  ballotfilem2  13285  ballotfilemfval0  13292  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemgun  13325  ballotfilemth  13338  ennnfonelemjn  13350  ennnfonelem1  13355  ennnfonelemhf1o  13361  imasplusg  13687  gsump1  14246  ringidvalg  14370  rmodislmod  14796  lspprid2  14857  isassa  15110  assamulgscmlem2  15150  sn0cld  15380  txval  15498  hmeontr  15556  comet  15742  cnmetdval  15772  sinhalfpilem  16035  cospi  16044  sincos4thpi  16084  sincos6thpi  16086  sincos3rdpi  16087  sinkpi  16091  reeflog  16109  logfac  16143  logbleb  16214  logblt  16215  sqrt2cxp2logb9e3  16228  birthdaylem2  16243  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  ppi1  16287  ppi1i  16289  ppi2i  16290  cht2  16293  cht3  16294  ppiqub  16310  chtqub  16313  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgsval2lem  16351  lgsquadlem2  16419  setsiedg  16515  wlkres  16842  trlreslem  16852  clwwlkccatlem  16863  eupthvdres  16938  eupth2lem3fi  16939  konigsbergvtx  16945  konigsbergiedg  16946  konigsberglem5  16955  konigsberg  16956  ex-ceil  16962  ex-fac  16964  012of  17245  2o01f  17246  nninfsellemqall  17281  nninfomni  17285  nninffeq  17286  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326