Theorem fveq1i 5640

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fveq1i	⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fveq1 5638	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1397  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq12i  5645  fvun2  5713  fvopab3ig  5720  fvsnun1  5850  fvsnun2  5851  fvpr1  5857  fvpr2  5858  fvpr1g  5859  fvpr2g  5860  fvtp1g  5861  fvtp2g  5862  fvtp3g  5863  fvtp2  5865  fvtp3  5866  ov  6140  ovigg  6141  ovg  6160  tfr2a  6486  tfrex  6533  frec0g  6562  freccllem  6567  frecsuclem  6571  caseinl  7289  caseinr  7290  ctssdccl  7309  addpiord  7535  mulpiord  7536  fseq1p1m1  10328  frec2uz0d  10660  frec2uzzd  10661  frec2uzsucd  10662  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdg0  10674  frecuzrdgsuc  10675  frecuzrdgg  10677  frecuzrdg0t  10683  frecuzrdgsuctlem  10684  0tonninf  10701  1tonninf  10702  inftonninf  10703  seq3val  10721  seqvalcd  10722  hashinfom  11039  hashennn  11041  hashfz1  11044  ccat1st1st  11217  cats1fvd  11346  shftidt  11393  resqrexlemf1  11568  resqrexlemfp1  11569  cbvsum  11920  fisumss  11952  fsumadd  11966  isumclim3  11983  cbvprod  12118  fprodssdc  12150  nninfctlemfo  12610  ialgr0  12615  algrp1  12617  ennnfonelem0  13025  ennnfonelemp1  13026  ennnfonelemom  13028  ctinfomlemom  13047  nninfdclemp1  13070  ndxarg  13104  strslfv2d  13124  prdsidlem  13529  prdsinvlem  13690  ringidvalg  13973  lidlvalg  14484  rspvalg  14485  znf1o  14664  mplnegfi  14718  upxp  14995  cnmetdval  15252  remetdval  15270  reeflog  15586  ushgredgedg  16076  ushgredgedgloop  16078  subgruhgredgdm  16120  vtxdumgrfival  16148  vtxd0nedgbfi  16149  vtxduspgrfvedgfi  16151  wlk1walkdom  16209  wlkres  16229  nninfnfiinf  16625