Theorem fveq1i 5508

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

Syntax hints:   = wceq 1353  ‘cfv 5208

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216

This theorem is referenced by:  fveq12i  5513  fvun2  5575  fvopab3ig  5582  fvsnun1  5705  fvsnun2  5706  fvpr1  5712  fvpr2  5713  fvpr1g  5714  fvpr2g  5715  fvtp1g  5716  fvtp2g  5717  fvtp3g  5718  fvtp2  5720  fvtp3  5721  ov  5984  ovigg  5985  ovg  6003  tfr2a  6312  tfrex  6359  frec0g  6388  freccllem  6393  frecsuclem  6397  caseinl  7080  caseinr  7081  ctssdccl  7100  addpiord  7290  mulpiord  7291  fseq1p1m1  10062  frec2uz0d  10367  frec2uzzd  10368  frec2uzsucd  10369  frecuzrdgrrn  10376  frec2uzrdg  10377  frecuzrdg0  10381  frecuzrdgsuc  10382  frecuzrdgg  10384  frecuzrdg0t  10390  frecuzrdgsuctlem  10391  0tonninf  10407  1tonninf  10408  inftonninf  10409  seq3val  10426  seqvalcd  10427  hashinfom  10724  hashennn  10726  hashfz1  10729  shftidt  10808  resqrexlemf1  10983  resqrexlemfp1  10984  cbvsum  11334  fisumss  11366  fsumadd  11380  isumclim3  11397  cbvprod  11532  fprodssdc  11564  ialgr0  12009  algrp1  12011  ennnfonelem0  12371  ennnfonelemp1  12372  ennnfonelemom  12374  ctinfomlemom  12393  nninfdclemp1  12416  ndxarg  12450  strslfv2d  12469  ringidvalg  12937  upxp  13323  cnmetdval  13580  remetdval  13590  reeflog  13835