Theorem fveq2i 5678

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

Syntax hints:   = wceq 1398  ‘cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  fveq12i  5681  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  algrflem  6438  tfr2a  6565  tfr0dm  6566  tfr0  6567  infisoti  7336  1prl  7886  1pru  7887  ltexprlemell  7929  ltexprlemelu  7930  recexprlemell  7953  recexprlemelu  7954  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlem2b  8045  suplocexprlemlub  8055  caucvgsr  8133  axcaucvg  8231  infrenegsupex  9944  fseq1p1m1  10450  fz0to4untppr  10480  rebtwn2zlemstep  10636  rebtwn2z  10638  fldiv4p1lem1div2  10689  frec2uzsucd  10787  frec2uzrdg  10795  frecuzrdgsuc  10800  frecuzrdgg  10802  frecuzrdgsuctlem  10809  frecfzennn  10812  0tonninf  10826  1tonninf  10827  seq3val  10846  seqvalcd  10847  seqf1oglem2  10906  facp1  11117  fac2  11118  fac3  11119  fac4  11120  4bc2eq6  11162  fihasheq0  11181  hashprg  11198  hashp1i  11200  pr0hash2ex  11205  hashfzo  11212  hashxp  11216  hashfibc  11232  zfz1isolemsplit  11235  hashtpgim  11242  hashtpg  11244  cats1lend  11484  rei  11609  imi  11610  sqrt1  11756  sqrt4  11757  sqrt9  11758  abs0  11768  absi  11769  infxrnegsupex  11973  fsumabs  12176  fsumrelem  12182  hashrabrex  12192  hashuni  12193  isumnn0nn  12204  mertenslem2  12247  ege2le3  12382  efsep  12402  efgt1p2  12406  efgt1p  12407  sin0  12440  cos0  12441  ef01bndlem  12467  cos2bnd  12471  sin4lt0  12478  m1bits  12671  nninfctlemfo  12761  eucalg  12781  prmind2  12842  dfphi2  12942  phiprmpw  12944  phimullem  12947  pockthlem  13079  pockthg  13080  prmunb  13085  ballotfilem1  13164  ballotfilem2  13172  ballotfilemfval0  13179  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemgun  13212  ballotfilemth  13225  ennnfonelemjn  13237  ennnfonelem1  13242  ennnfonelemhf1o  13248  imasplusg  13572  gfsump1  14108  ringidvalg  14204  rmodislmod  14625  lspprid2  14686  sn0cld  15128  txval  15246  hmeontr  15304  comet  15490  cnmetdval  15520  sinhalfpilem  15782  cospi  15791  sincos4thpi  15831  sincos6thpi  15833  sincos3rdpi  15834  sinkpi  15838  reeflog  15854  logbleb  15952  logblt  15953  sqrt2cxp2logb9e3  15966  lgsval2lem  16009  lgsquadlem2  16077  setsiedg  16173  wlkres  16500  trlreslem  16510  clwwlkccatlem  16521  eupthvdres  16596  eupth2lem3fi  16597  konigsbergvtx  16603  konigsbergiedg  16604  konigsberglem5  16613  konigsberg  16614  ex-ceil  16620  ex-fac  16622  012of  16893  2o01f  16894  nninfsellemqall  16919  nninfomni  16923  nninffeq  16924  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963