Theorem fveq1i 5517

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 5515	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( G ` A )

Syntax hints:   = wceq 1353   ` cfv 5217

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 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  fveq12i  5522  fvun2  5584  fvopab3ig  5591  fvsnun1  5714  fvsnun2  5715  fvpr1  5721  fvpr2  5722  fvpr1g  5723  fvpr2g  5724  fvtp1g  5725  fvtp2g  5726  fvtp3g  5727  fvtp2  5729  fvtp3  5730  ov  5994  ovigg  5995  ovg  6013  tfr2a  6322  tfrex  6369  frec0g  6398  freccllem  6403  frecsuclem  6407  caseinl  7090  caseinr  7091  ctssdccl  7110  addpiord  7315  mulpiord  7316  fseq1p1m1  10094  frec2uz0d  10399  frec2uzzd  10400  frec2uzsucd  10401  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdg0  10413  frecuzrdgsuc  10414  frecuzrdgg  10416  frecuzrdg0t  10422  frecuzrdgsuctlem  10423  0tonninf  10439  1tonninf  10440  inftonninf  10441  seq3val  10458  seqvalcd  10459  hashinfom  10758  hashennn  10760  hashfz1  10763  shftidt  10842  resqrexlemf1  11017  resqrexlemfp1  11018  cbvsum  11368  fisumss  11400  fsumadd  11414  isumclim3  11431  cbvprod  11566  fprodssdc  11598  ialgr0  12044  algrp1  12046  ennnfonelem0  12406  ennnfonelemp1  12407  ennnfonelemom  12409  ctinfomlemom  12428  nninfdclemp1  12451  ndxarg  12485  strslfv2d  12505  ringidvalg  13144  upxp  13775  cnmetdval  14032  remetdval  14042  reeflog  14287