Theorem fveq2i 5597

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

Syntax hints:   = wceq 1373  ‘cfv 5285

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-br 4055  df-iota 5246  df-fv 5293

This theorem is referenced by:  fveq12i  5600  ot1stg  6256  ot2ndg  6257  ot3rdgg  6258  algrflem  6333  tfr2a  6425  tfr0dm  6426  tfr0  6427  infisoti  7155  1prl  7698  1pru  7699  ltexprlemell  7741  ltexprlemelu  7742  recexprlemell  7765  recexprlemelu  7766  cauappcvgprlemm  7788  cauappcvgprlemopl  7789  cauappcvgprlemlol  7790  cauappcvgprlemopu  7791  cauappcvgprlemupu  7792  cauappcvgprlemdisj  7794  cauappcvgprlemloc  7795  cauappcvgprlemladdfu  7797  cauappcvgprlemladdfl  7798  cauappcvgprlemladdru  7799  cauappcvgprlem2  7803  caucvgprlemm  7811  caucvgprlemopl  7812  caucvgprlemlol  7813  caucvgprlemopu  7814  caucvgprlemupu  7815  caucvgprlemdisj  7817  caucvgprlemloc  7818  caucvgprlemladdfu  7820  caucvgprlem2  7823  caucvgprprlemell  7828  caucvgprprlemelu  7829  caucvgprprlemml  7837  caucvgprprlemmu  7838  caucvgprprlemexbt  7849  caucvgprprlem2  7853  suplocexprlem2b  7857  suplocexprlemlub  7867  caucvgsr  7945  axcaucvg  8043  infrenegsupex  9745  fseq1p1m1  10246  fz0to4untppr  10276  rebtwn2zlemstep  10427  rebtwn2z  10429  fldiv4p1lem1div2  10480  frec2uzsucd  10578  frec2uzrdg  10586  frecuzrdgsuc  10591  frecuzrdgg  10593  frecuzrdgsuctlem  10600  frecfzennn  10603  0tonninf  10617  1tonninf  10618  seq3val  10637  seqvalcd  10638  seqf1oglem2  10697  facp1  10907  fac2  10908  fac3  10909  fac4  10910  4bc2eq6  10951  fihasheq0  10970  hashprg  10985  hashp1i  10987  pr0hash2ex  10992  hashfzo  10999  hashxp  11003  zfz1isolemsplit  11015  rei  11295  imi  11296  sqrt1  11442  sqrt4  11443  sqrt9  11444  abs0  11454  absi  11455  infxrnegsupex  11659  fsumabs  11861  fsumrelem  11867  hashrabrex  11877  hashuni  11878  isumnn0nn  11889  mertenslem2  11932  ege2le3  12067  efsep  12087  efgt1p2  12091  efgt1p  12092  sin0  12125  cos0  12126  ef01bndlem  12152  cos2bnd  12156  sin4lt0  12163  m1bits  12356  nninfctlemfo  12446  eucalg  12466  prmind2  12527  dfphi2  12627  phiprmpw  12629  phimullem  12632  pockthlem  12764  pockthg  12765  prmunb  12770  ennnfonelemjn  12858  ennnfonelem1  12863  ennnfonelemhf1o  12869  imasplusg  13225  ringidvalg  13808  rmodislmod  14198  lspprid2  14259  sn0cld  14694  txval  14812  hmeontr  14870  comet  15056  cnmetdval  15086  sinhalfpilem  15348  cospi  15357  sincos4thpi  15397  sincos6thpi  15399  sincos3rdpi  15400  sinkpi  15404  reeflog  15420  logbleb  15518  logblt  15519  sqrt2cxp2logb9e3  15532  lgsval2lem  15572  lgsquadlem2  15640  ex-ceil  15832  ex-fac  15834  012of  16100  2o01f  16101  nninfsellemqall  16124  nninfomni  16128  nninffeq  16129  isomninnlem  16141  iswomninnlem  16160  ismkvnnlem  16163