Theorem fveq2i 5578

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

Syntax hints:   = wceq 1372  ‘cfv 5270

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278

This theorem is referenced by:  fveq12i  5581  ot1stg  6237  ot2ndg  6238  ot3rdgg  6239  algrflem  6314  tfr2a  6406  tfr0dm  6407  tfr0  6408  infisoti  7133  1prl  7667  1pru  7668  ltexprlemell  7710  ltexprlemelu  7711  recexprlemell  7734  recexprlemelu  7735  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlem2  7772  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlem2  7792  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemexbt  7818  caucvgprprlem2  7822  suplocexprlem2b  7826  suplocexprlemlub  7836  caucvgsr  7914  axcaucvg  8012  infrenegsupex  9714  fseq1p1m1  10215  fz0to4untppr  10245  rebtwn2zlemstep  10393  rebtwn2z  10395  fldiv4p1lem1div2  10446  frec2uzsucd  10544  frec2uzrdg  10552  frecuzrdgsuc  10557  frecuzrdgg  10559  frecuzrdgsuctlem  10566  frecfzennn  10569  0tonninf  10583  1tonninf  10584  seq3val  10603  seqvalcd  10604  seqf1oglem2  10663  facp1  10873  fac2  10874  fac3  10875  fac4  10876  4bc2eq6  10917  fihasheq0  10936  hashprg  10951  hashp1i  10953  pr0hash2ex  10958  hashfzo  10965  hashxp  10969  zfz1isolemsplit  10981  rei  11152  imi  11153  sqrt1  11299  sqrt4  11300  sqrt9  11301  abs0  11311  absi  11312  infxrnegsupex  11516  fsumabs  11718  fsumrelem  11724  hashrabrex  11734  hashuni  11735  isumnn0nn  11746  mertenslem2  11789  ege2le3  11924  efsep  11944  efgt1p2  11948  efgt1p  11949  sin0  11982  cos0  11983  ef01bndlem  12009  cos2bnd  12013  sin4lt0  12020  m1bits  12213  nninfctlemfo  12303  eucalg  12323  prmind2  12384  dfphi2  12484  phiprmpw  12486  phimullem  12489  pockthlem  12621  pockthg  12622  prmunb  12627  ennnfonelemjn  12715  ennnfonelem1  12720  ennnfonelemhf1o  12726  imasplusg  13082  ringidvalg  13665  rmodislmod  14055  lspprid2  14116  sn0cld  14551  txval  14669  hmeontr  14727  comet  14913  cnmetdval  14943  sinhalfpilem  15205  cospi  15214  sincos4thpi  15254  sincos6thpi  15256  sincos3rdpi  15257  sinkpi  15261  reeflog  15277  logbleb  15375  logblt  15376  sqrt2cxp2logb9e3  15389  lgsval2lem  15429  lgsquadlem2  15497  ex-ceil  15595  ex-fac  15597  012of  15863  2o01f  15864  nninfsellemqall  15885  nninfomni  15889  nninffeq  15890  isomninnlem  15902  iswomninnlem  15921  ismkvnnlem  15924