Theorem fveq1i 5513

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

Syntax hints:   = wceq 1353  ‘cfv 5213

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221

This theorem is referenced by:  fveq12i  5518  fvun2  5580  fvopab3ig  5587  fvsnun1  5710  fvsnun2  5711  fvpr1  5717  fvpr2  5718  fvpr1g  5719  fvpr2g  5720  fvtp1g  5721  fvtp2g  5722  fvtp3g  5723  fvtp2  5725  fvtp3  5726  ov  5989  ovigg  5990  ovg  6008  tfr2a  6317  tfrex  6364  frec0g  6393  freccllem  6398  frecsuclem  6402  caseinl  7085  caseinr  7086  ctssdccl  7105  addpiord  7310  mulpiord  7311  fseq1p1m1  10087  frec2uz0d  10392  frec2uzzd  10393  frec2uzsucd  10394  frecuzrdgrrn  10401  frec2uzrdg  10402  frecuzrdg0  10406  frecuzrdgsuc  10407  frecuzrdgg  10409  frecuzrdg0t  10415  frecuzrdgsuctlem  10416  0tonninf  10432  1tonninf  10433  inftonninf  10434  seq3val  10451  seqvalcd  10452  hashinfom  10749  hashennn  10751  hashfz1  10754  shftidt  10833  resqrexlemf1  11008  resqrexlemfp1  11009  cbvsum  11359  fisumss  11391  fsumadd  11405  isumclim3  11422  cbvprod  11557  fprodssdc  11589  ialgr0  12034  algrp1  12036  ennnfonelem0  12396  ennnfonelemp1  12397  ennnfonelemom  12399  ctinfomlemom  12418  nninfdclemp1  12441  ndxarg  12475  strslfv2d  12495  ringidvalg  13044  upxp  13554  cnmetdval  13811  remetdval  13821  reeflog  14066