Theorem fveq1i 5576

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

Syntax hints:   = wceq 1372  ‘cfv 5270

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278

This theorem is referenced by:  fveq12i  5581  fvun2  5645  fvopab3ig  5652  fvsnun1  5780  fvsnun2  5781  fvpr1  5787  fvpr2  5788  fvpr1g  5789  fvpr2g  5790  fvtp1g  5791  fvtp2g  5792  fvtp3g  5793  fvtp2  5795  fvtp3  5796  ov  6064  ovigg  6065  ovg  6084  tfr2a  6406  tfrex  6453  frec0g  6482  freccllem  6487  frecsuclem  6491  caseinl  7192  caseinr  7193  ctssdccl  7212  addpiord  7428  mulpiord  7429  fseq1p1m1  10215  frec2uz0d  10542  frec2uzzd  10543  frec2uzsucd  10544  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdg0  10556  frecuzrdgsuc  10557  frecuzrdgg  10559  frecuzrdg0t  10565  frecuzrdgsuctlem  10566  0tonninf  10583  1tonninf  10584  inftonninf  10585  seq3val  10603  seqvalcd  10604  hashinfom  10921  hashennn  10923  hashfz1  10926  shftidt  11086  resqrexlemf1  11261  resqrexlemfp1  11262  cbvsum  11613  fisumss  11645  fsumadd  11659  isumclim3  11676  cbvprod  11811  fprodssdc  11843  nninfctlemfo  12303  ialgr0  12308  algrp1  12310  ennnfonelem0  12718  ennnfonelemp1  12719  ennnfonelemom  12721  ctinfomlemom  12740  nninfdclemp1  12763  ndxarg  12797  strslfv2d  12817  prdsidlem  13221  prdsinvlem  13382  ringidvalg  13665  lidlvalg  14175  rspvalg  14176  znf1o  14355  mplnegfi  14409  upxp  14686  cnmetdval  14943  remetdval  14961  reeflog  15277  nninfnfiinf  15893