Theorem fveq2i 5510

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

Syntax hints:   = wceq 1353  ‘cfv 5208

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216

This theorem is referenced by:  fveq12i  5513  ot1stg  6143  ot2ndg  6144  ot3rdgg  6145  algrflem  6220  tfr2a  6312  tfr0dm  6313  tfr0  6314  infisoti  7021  1prl  7529  1pru  7530  ltexprlemell  7572  ltexprlemelu  7573  recexprlemell  7596  recexprlemelu  7597  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemopu  7622  cauappcvgprlemupu  7623  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  cauappcvgprlem2  7634  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemopu  7645  caucvgprlemupu  7646  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemladdfu  7651  caucvgprlem2  7654  caucvgprprlemell  7659  caucvgprprlemelu  7660  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemexbt  7680  caucvgprprlem2  7684  suplocexprlem2b  7688  suplocexprlemlub  7698  caucvgsr  7776  axcaucvg  7874  infrenegsupex  9567  fseq1p1m1  10064  fz0to4untppr  10094  rebtwn2zlemstep  10223  rebtwn2z  10225  fldiv4p1lem1div2  10275  frec2uzsucd  10371  frec2uzrdg  10379  frecuzrdgsuc  10384  frecuzrdgg  10386  frecuzrdgsuctlem  10393  frecfzennn  10396  0tonninf  10409  1tonninf  10410  seq3val  10428  seqvalcd  10429  facp1  10678  fac2  10679  fac3  10680  fac4  10681  4bc2eq6  10722  fihasheq0  10741  hashprg  10756  hashp1i  10758  pr0hash2ex  10763  hashfzo  10770  hashxp  10774  zfz1isolemsplit  10786  rei  10876  imi  10877  sqrt1  11023  sqrt4  11024  sqrt9  11025  abs0  11035  absi  11036  infxrnegsupex  11239  fsumabs  11441  fsumrelem  11447  hashrabrex  11457  hashuni  11458  isumnn0nn  11469  mertenslem2  11512  ege2le3  11647  efsep  11667  efgt1p2  11671  efgt1p  11672  sin0  11705  cos0  11706  ef01bndlem  11732  cos2bnd  11736  sin4lt0  11742  eucalg  12026  prmind2  12087  dfphi2  12187  phiprmpw  12189  phimullem  12192  pockthlem  12321  pockthg  12322  prmunb  12327  ennnfonelemjn  12370  ennnfonelem1  12375  ennnfonelemhf1o  12381  ringidvalg  12941  sn0cld  13208  txval  13326  hmeontr  13384  comet  13570  cnmetdval  13600  sinhalfpilem  13783  cospi  13792  sincos4thpi  13832  sincos6thpi  13834  sincos3rdpi  13835  sinkpi  13839  reeflog  13855  logbleb  13950  logblt  13951  sqrt2cxp2logb9e3  13964  lgsval2lem  13982  ex-ceil  14038  ex-fac  14040  012of  14305  2o01f  14306  nninfsellemqall  14325  nninfomni  14329  nninffeq  14330  isomninnlem  14339  iswomninnlem  14358  ismkvnnlem  14361