Theorem fveq1i 5497

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

Syntax hints:   = wceq 1348  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206

This theorem is referenced by:  fveq12i  5502  fvun2  5563  fvopab3ig  5570  fvsnun1  5693  fvsnun2  5694  fvpr1  5700  fvpr2  5701  fvpr1g  5702  fvpr2g  5703  fvtp1g  5704  fvtp2g  5705  fvtp3g  5706  fvtp2  5708  fvtp3  5709  ov  5972  ovigg  5973  ovg  5991  tfr2a  6300  tfrex  6347  frec0g  6376  freccllem  6381  frecsuclem  6385  caseinl  7068  caseinr  7069  ctssdccl  7088  addpiord  7278  mulpiord  7279  fseq1p1m1  10050  frec2uz0d  10355  frec2uzzd  10356  frec2uzsucd  10357  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdg0  10369  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdg0t  10378  frecuzrdgsuctlem  10379  0tonninf  10395  1tonninf  10396  inftonninf  10397  seq3val  10414  seqvalcd  10415  hashinfom  10712  hashennn  10714  hashfz1  10717  shftidt  10797  resqrexlemf1  10972  resqrexlemfp1  10973  cbvsum  11323  fisumss  11355  fsumadd  11369  isumclim3  11386  cbvprod  11521  fprodssdc  11553  ialgr0  11998  algrp1  12000  ennnfonelem0  12360  ennnfonelemp1  12361  ennnfonelemom  12363  ctinfomlemom  12382  nninfdclemp1  12405  ndxarg  12439  strslfv2d  12458  upxp  13066  cnmetdval  13323  remetdval  13333  reeflog  13578