Theorem fveq1i 5422

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

Syntax hints:   = wceq 1331  ‘cfv 5123

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131

This theorem is referenced by:  fveq12i  5427  fvun2  5488  fvopab3ig  5495  fvsnun1  5617  fvsnun2  5618  fvpr1  5624  fvpr2  5625  fvpr1g  5626  fvpr2g  5627  fvtp1g  5628  fvtp2g  5629  fvtp3g  5630  fvtp2  5632  fvtp3  5633  ov  5890  ovigg  5891  ovg  5909  tfr2a  6218  tfrex  6265  frec0g  6294  freccllem  6299  frecsuclem  6303  caseinl  6976  caseinr  6977  ctssdccl  6996  addpiord  7124  mulpiord  7125  fseq1p1m1  9874  frec2uz0d  10172  frec2uzzd  10173  frec2uzsucd  10174  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdg0  10186  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdg0t  10195  frecuzrdgsuctlem  10196  0tonninf  10212  1tonninf  10213  inftonninf  10214  seq3val  10231  seqvalcd  10232  hashinfom  10524  hashennn  10526  hashfz1  10529  shftidt  10605  resqrexlemf1  10780  resqrexlemfp1  10781  cbvsum  11129  fisumss  11161  fsumadd  11175  isumclim3  11192  cbvprod  11327  ialgr0  11725  algrp1  11727  ennnfonelem0  11918  ennnfonelemp1  11919  ennnfonelemom  11921  ctinfomlemom  11940  ndxarg  11982  strslfv2d  12001  upxp  12441  cnmetdval  12698  remetdval  12708