Theorem fveq1i 5306

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

Syntax hints:   = wceq 1289  ‘cfv 5015

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-uni 3654  df-br 3846  df-iota 4980  df-fv 5023

This theorem is referenced by:  fveq12i  5311  fvun2  5371  fvopab3ig  5378  fvsnun1  5494  fvsnun2  5495  fvpr1  5501  fvpr2  5502  fvpr1g  5503  fvpr2g  5504  fvtp1g  5505  fvtp2g  5506  fvtp3g  5507  fvtp2  5509  fvtp3  5510  ov  5764  ovigg  5765  ovg  5783  tfr2a  6086  tfrex  6133  frec0g  6162  freccllem  6167  frecsuclem  6171  addpiord  6875  mulpiord  6876  fseq1p1m1  9508  frec2uz0d  9806  frec2uzzd  9807  frec2uzsucd  9808  frecuzrdgrrn  9815  frec2uzrdg  9816  frecuzrdg0  9820  frecuzrdgsuc  9821  frecuzrdgg  9823  frecuzrdg0t  9829  frecuzrdgsuctlem  9830  0tonninf  9845  1tonninf  9846  inftonninf  9847  iseqvalt  9873  seq3val  9874  hashinfom  10186  hashennn  10188  hashfz1  10191  shftidt  10267  resqrexlemf1  10441  resqrexlemfp1  10442  cbvsum  10749  fisumss  10784  fsumadd  10800  isumclim3  10817  ialgr0  11304  ialgrp1  11306  ndxarg  11519  strslfv2d  11536