Theorem fveq1i 5691

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

Syntax hints:   = wceq 1402  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  fveq12i  5696  fvun2  5764  fvopab3ig  5773  fvsnun1  5903  fvsnun2  5904  fvpr1  5910  fvpr2  5911  fvpr1g  5912  fvpr2g  5913  fvtp1g  5914  fvtp2g  5915  fvtp3g  5916  fvtp2  5918  fvtp3  5919  ov  6198  ovigg  6199  ovg  6218  suppsnopdc  6480  tfr2a  6582  tfrex  6629  frec0g  6658  freccllem  6663  frecsuclem  6667  caseinl  7421  caseinr  7422  ctssdccl  7441  addpiord  7673  mulpiord  7674  fseq1p1m1  10479  frec2uz0d  10814  frec2uzzd  10815  frec2uzsucd  10816  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdg0  10828  frecuzrdgsuc  10829  frecuzrdgg  10831  frecuzrdg0t  10837  frecuzrdgsuctlem  10838  0tonninf  10855  1tonninf  10856  inftonninf  10857  seq3val  10875  seqvalcd  10876  hashinfom  11195  hashennn  11197  hashfz1  11200  ccat1st1st  11387  cats1fvd  11516  shftidt  11576  resqrexlemf1  11752  resqrexlemfp1  11753  cbvsum  12104  fisumss  12137  fsumadd  12151  isumclim3  12168  cbvprod  12303  fprodssdc  12335  nninfctlemfo  12795  ialgr0  12800  algrp1  12802  ennnfonelem0  13274  ennnfonelemp1  13275  ennnfonelemom  13277  ctinfomlemom  13296  nninfdclemp1  13319  ndxarg  13353  strslfv2d  13373  gsumconstcmn  14143  prdsidlem  14170  prdsinvlem  14173  ringidvalg  14239  lidlvalg  14780  rspvalg  14781  znf1o  14958  mplnegfi  15019  upxp  15296  cnmetdval  15553  remetdval  15571  reeflog  15887  logfac  15918  ushgredgedg  16381  ushgredgedgloop  16383  subgruhgredgdm  16425  vtxdumgrfival  16453  vtxd0nedgbfi  16454  vtxduspgrfvedgfi  16456  wlk1walkdom  16514  wlkres  16534  depindlem1  16661  nninfnfiinf  16971