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  9994  fseq1p1m1  10501  fz0to4untppr  10531  rebtwn2zlemstep  10687  rebtwn2z  10689  fldiv4p1lem1div2  10740  frec2uzsucd  10838  frec2uzrdg  10846  frecuzrdgsuc  10851  frecuzrdgg  10853  frecuzrdgsuctlem  10860  frecfzennn  10863  0tonninf  10877  1tonninf  10878  seq3val  10897  seqvalcd  10898  seqf1oglem2  10957  facp1  11168  fac2  11169  fac3  11170  fac4  11171  4bc2eq6  11213  fihasheq0  11232  hashprg  11249  hashp1i  11251  pr0hash2ex  11256  hashfzo  11263  hashxp  11267  hashfibc  11283  hashf1lem2  11286  zfz1isolemsplit  11290  hashtpgim  11297  hashtpg  11299  cats1lend  11539  rei  11665  imi  11666  sqrt1  11812  sqrt4  11813  sqrt9  11814  abs0  11824  absi  11825  infxrnegsupex  12029  fsumabs  12232  fsumrelem  12238  hashrabrex  12248  hashuni  12249  isumnn0nn  12260  mertenslem2  12303  ege2le3  12438  efsep  12458  efgt1p2  12462  efgt1p  12463  sin0  12496  cos0  12497  ef01bndlem  12523  cos2bnd  12527  sin4lt0  12534  m1bits  12727  nninfctlemfo  12817  eucalg  12837  prmind2  12898  dfphi2  12998  phiprmpw  13000  phimullem  13003  pockthlem  13135  pockthg  13136  prmunb  13141  ballotfilem1  13220  ballotfilem2  13228  ballotfilemfval0  13235  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemgun  13268  ballotfilemth  13281  ennnfonelemjn  13293  ennnfonelem1  13298  ennnfonelemhf1o  13304  imasplusg  13629  gsump1  14157  ringidvalg  14264  rmodislmod  14688  lspprid2  14749  isassa  15002  assamulgscmlem2  15042  sn0cld  15238  txval  15356  hmeontr  15414  comet  15600  cnmetdval  15630  sinhalfpilem  15892  cospi  15901  sincos4thpi  15941  sincos6thpi  15943  sincos3rdpi  15944  sinkpi  15948  reeflog  15964  logfac  15995  logbleb  16063  logblt  16064  sqrt2cxp2logb9e3  16077  birthdaylem2  16088  lgsval2lem  16129  lgsquadlem2  16197  setsiedg  16293  wlkres  16620  trlreslem  16630  clwwlkccatlem  16641  eupthvdres  16716  eupth2lem3fi  16717  konigsbergvtx  16723  konigsbergiedg  16724  konigsberglem5  16733  konigsberg  16734  ex-ceil  16740  ex-fac  16742  012of  17023  2o01f  17024  nninfsellemqall  17058  nninfomni  17062  nninffeq  17063  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102