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  11181  imi  11182  sqrt1  11328  sqrt4  11329  sqrt9  11330  abs0  11340  absi  11341  infxrnegsupex  11545  fsumabs  11747  fsumrelem  11753  hashrabrex  11763  hashuni  11764  isumnn0nn  11775  mertenslem2  11818  ege2le3  11953  efsep  11973  efgt1p2  11977  efgt1p  11978  sin0  12011  cos0  12012  ef01bndlem  12038  cos2bnd  12042  sin4lt0  12049  m1bits  12242  nninfctlemfo  12332  eucalg  12352  prmind2  12413  dfphi2  12513  phiprmpw  12515  phimullem  12518  pockthlem  12650  pockthg  12651  prmunb  12656  ennnfonelemjn  12744  ennnfonelem1  12749  ennnfonelemhf1o  12755  imasplusg  13111  ringidvalg  13694  rmodislmod  14084  lspprid2  14145  sn0cld  14580  txval  14698  hmeontr  14756  comet  14942  cnmetdval  14972  sinhalfpilem  15234  cospi  15243  sincos4thpi  15283  sincos6thpi  15285  sincos3rdpi  15286  sinkpi  15290  reeflog  15306  logbleb  15404  logblt  15405  sqrt2cxp2logb9e3  15418  lgsval2lem  15458  lgsquadlem2  15526  ex-ceil  15624  ex-fac  15626  012of  15892  2o01f  15893  nninfsellemqall  15914  nninfomni  15918  nninffeq  15919  isomninnlem  15931  iswomninnlem  15950  ismkvnnlem  15953