Theorem fveq1i 5649

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

Syntax hints:   = wceq 1398  ‘cfv 5333

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq12i  5654  fvun2  5722  fvopab3ig  5729  fvsnun1  5859  fvsnun2  5860  fvpr1  5866  fvpr2  5867  fvpr1g  5868  fvpr2g  5869  fvtp1g  5870  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  ov  6151  ovigg  6152  ovg  6171  suppsnopdc  6428  tfr2a  6530  tfrex  6577  frec0g  6606  freccllem  6611  frecsuclem  6615  caseinl  7333  caseinr  7334  ctssdccl  7353  addpiord  7579  mulpiord  7580  fseq1p1m1  10374  frec2uz0d  10707  frec2uzzd  10708  frec2uzsucd  10709  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdg0  10721  frecuzrdgsuc  10722  frecuzrdgg  10724  frecuzrdg0t  10730  frecuzrdgsuctlem  10731  0tonninf  10748  1tonninf  10749  inftonninf  10750  seq3val  10768  seqvalcd  10769  hashinfom  11086  hashennn  11088  hashfz1  11091  ccat1st1st  11267  cats1fvd  11396  shftidt  11456  resqrexlemf1  11631  resqrexlemfp1  11632  cbvsum  11983  fisumss  12016  fsumadd  12030  isumclim3  12047  cbvprod  12182  fprodssdc  12214  nninfctlemfo  12674  ialgr0  12679  algrp1  12681  ennnfonelem0  13089  ennnfonelemp1  13090  ennnfonelemom  13092  ctinfomlemom  13111  nninfdclemp1  13134  ndxarg  13168  strslfv2d  13188  prdsidlem  13593  prdsinvlem  13754  ringidvalg  14038  lidlvalg  14550  rspvalg  14551  znf1o  14730  mplnegfi  14789  upxp  15066  cnmetdval  15323  remetdval  15341  reeflog  15657  ushgredgedg  16150  ushgredgedgloop  16152  subgruhgredgdm  16194  vtxdumgrfival  16222  vtxd0nedgbfi  16223  vtxduspgrfvedgfi  16225  wlk1walkdom  16283  wlkres  16303  depindlem1  16430  nninfnfiinf  16732