Theorem fveq1i 5516

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	|- F = G

Assertion

Ref	Expression
fveq1i	|- ( F ` A ) = ( G ` A )

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 |- F = G
2		fveq1 5514	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( G ` A )

Syntax hints:   = wceq 1353   ` cfv 5216

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 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  fveq12i  5521  fvun2  5583  fvopab3ig  5590  fvsnun1  5713  fvsnun2  5714  fvpr1  5720  fvpr2  5721  fvpr1g  5722  fvpr2g  5723  fvtp1g  5724  fvtp2g  5725  fvtp3g  5726  fvtp2  5728  fvtp3  5729  ov  5993  ovigg  5994  ovg  6012  tfr2a  6321  tfrex  6368  frec0g  6397  freccllem  6402  frecsuclem  6406  caseinl  7089  caseinr  7090  ctssdccl  7109  addpiord  7314  mulpiord  7315  fseq1p1m1  10093  frec2uz0d  10398  frec2uzzd  10399  frec2uzsucd  10400  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdg0  10412  frecuzrdgsuc  10413  frecuzrdgg  10415  frecuzrdg0t  10421  frecuzrdgsuctlem  10422  0tonninf  10438  1tonninf  10439  inftonninf  10440  seq3val  10457  seqvalcd  10458  hashinfom  10757  hashennn  10759  hashfz1  10762  shftidt  10841  resqrexlemf1  11016  resqrexlemfp1  11017  cbvsum  11367  fisumss  11399  fsumadd  11413  isumclim3  11430  cbvprod  11565  fprodssdc  11597  ialgr0  12043  algrp1  12045  ennnfonelem0  12405  ennnfonelemp1  12406  ennnfonelemom  12408  ctinfomlemom  12427  nninfdclemp1  12450  ndxarg  12484  strslfv2d  12504  ringidvalg  13142  upxp  13742  cnmetdval  13999  remetdval  14009  reeflog  14254