Theorem fveq2i 5698

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

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

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 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12i  5701  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  algrflem  6465  tfr2a  6592  tfr0dm  6593  tfr0  6594  infisoti  7372  1prl  7922  1pru  7923  ltexprlemell  7965  ltexprlemelu  7966  recexprlemell  7989  recexprlemelu  7990  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlem2b  8081  suplocexprlemlub  8091  caucvgsr  8169  axcaucvg  8267  infrenegsupex  10003  fseq1p1m1  10511  fz0to4untppr  10541  rebtwn2zlemstep  10697  rebtwn2z  10699  fldiv4p1lem1div2  10753  frec2uzsucd  10851  frec2uzrdg  10859  frecuzrdgsuc  10864  frecuzrdgg  10866  frecuzrdgsuctlem  10873  frecfzennn  10876  0tonninf  10890  1tonninf  10891  seq3val  10910  seqvalcd  10911  seqf1oglem2  10970  facp1  11182  fac2  11183  fac3  11184  fac4  11185  4bc2eq6  11227  fihasheq0  11246  hashprg  11263  hashp1i  11265  pr0hash2ex  11270  hashfzo  11277  hashxp  11281  hashfibc  11297  hashf1lem2  11300  zfz1isolemsplit  11304  hashtpgim  11311  hashtpg  11313  cats1lend  11553  rei  11679  imi  11680  sqrt1  11826  sqrt4  11827  sqrt9  11828  abs0  11838  absi  11839  infxrnegsupex  12045  fsumabs  12248  fsumrelem  12254  hashrabrex  12264  hashuni  12265  isumnn0nn  12276  mertenslem2  12319  ege2le3  12454  efsep  12474  efgt1p2  12478  efgt1p  12479  sin0  12512  cos0  12513  ef01bndlem  12539  cos2bnd  12543  sin4lt0  12550  m1bits  12743  nninfctlemfo  12833  eucalg  12853  prmind2  12914  dfphi2  13018  phiprmpw  13020  phimullem  13023  pockthlem  13155  pockthg  13156  prmunb  13161  ballotfilem1  13269  ballotfilem2  13277  ballotfilemfval0  13284  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemgun  13317  ballotfilemth  13330  ennnfonelemjn  13342  ennnfonelem1  13347  ennnfonelemhf1o  13353  imasplusg  13678  gsump1  14206  ringidvalg  14313  rmodislmod  14737  lspprid2  14798  isassa  15051  assamulgscmlem2  15091  sn0cld  15287  txval  15405  hmeontr  15463  comet  15649  cnmetdval  15679  sinhalfpilem  15942  cospi  15951  sincos4thpi  15991  sincos6thpi  15993  sincos3rdpi  15994  sinkpi  15998  reeflog  16014  logfac  16048  logbleb  16116  logblt  16117  sqrt2cxp2logb9e3  16130  birthdaylem2  16145  ppiprm  16170  ppinprm  16171  ppi1  16176  ppi1i  16177  ppi2i  16178  ppiqub  16194  lgsval2lem  16227  lgsquadlem2  16295  setsiedg  16391  wlkres  16718  trlreslem  16728  clwwlkccatlem  16739  eupthvdres  16814  eupth2lem3fi  16815  konigsbergvtx  16821  konigsbergiedg  16822  konigsberglem5  16831  konigsberg  16832  ex-ceil  16838  ex-fac  16840  012of  17121  2o01f  17122  nninfsellemqall  17156  nninfomni  17160  nninffeq  17161  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200