Theorem fveq1i 5528

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

Syntax hints:   = wceq 1363   ` cfv 5228

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236

This theorem is referenced by:  fveq12i  5533  fvun2  5596  fvopab3ig  5603  fvsnun1  5726  fvsnun2  5727  fvpr1  5733  fvpr2  5734  fvpr1g  5735  fvpr2g  5736  fvtp1g  5737  fvtp2g  5738  fvtp3g  5739  fvtp2  5741  fvtp3  5742  ov  6007  ovigg  6008  ovg  6026  tfr2a  6335  tfrex  6382  frec0g  6411  freccllem  6416  frecsuclem  6420  caseinl  7103  caseinr  7104  ctssdccl  7123  addpiord  7328  mulpiord  7329  fseq1p1m1  10107  frec2uz0d  10412  frec2uzzd  10413  frec2uzsucd  10414  frecuzrdgrrn  10421  frec2uzrdg  10422  frecuzrdg0  10426  frecuzrdgsuc  10427  frecuzrdgg  10429  frecuzrdg0t  10435  frecuzrdgsuctlem  10436  0tonninf  10452  1tonninf  10453  inftonninf  10454  seq3val  10471  seqvalcd  10472  hashinfom  10771  hashennn  10773  hashfz1  10776  shftidt  10855  resqrexlemf1  11030  resqrexlemfp1  11031  cbvsum  11381  fisumss  11413  fsumadd  11427  isumclim3  11444  cbvprod  11579  fprodssdc  11611  ialgr0  12057  algrp1  12059  ennnfonelem0  12419  ennnfonelemp1  12420  ennnfonelemom  12422  ctinfomlemom  12441  nninfdclemp1  12464  ndxarg  12498  strslfv2d  12518  ringidvalg  13208  lidlvalg  13655  rspvalg  13656  upxp  14043  cnmetdval  14300  remetdval  14310  reeflog  14555