Theorem fveq1i 5600

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

Syntax hints:   = wceq 1373   ` cfv 5290

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298

This theorem is referenced by:  fveq12i  5605  fvun2  5669  fvopab3ig  5676  fvsnun1  5804  fvsnun2  5805  fvpr1  5811  fvpr2  5812  fvpr1g  5813  fvpr2g  5814  fvtp1g  5815  fvtp2g  5816  fvtp3g  5817  fvtp2  5819  fvtp3  5820  ov  6088  ovigg  6089  ovg  6108  tfr2a  6430  tfrex  6477  frec0g  6506  freccllem  6511  frecsuclem  6515  caseinl  7219  caseinr  7220  ctssdccl  7239  addpiord  7464  mulpiord  7465  fseq1p1m1  10251  frec2uz0d  10581  frec2uzzd  10582  frec2uzsucd  10583  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdg0  10595  frecuzrdgsuc  10596  frecuzrdgg  10598  frecuzrdg0t  10604  frecuzrdgsuctlem  10605  0tonninf  10622  1tonninf  10623  inftonninf  10624  seq3val  10642  seqvalcd  10643  hashinfom  10960  hashennn  10962  hashfz1  10965  ccat1st1st  11131  shftidt  11259  resqrexlemf1  11434  resqrexlemfp1  11435  cbvsum  11786  fisumss  11818  fsumadd  11832  isumclim3  11849  cbvprod  11984  fprodssdc  12016  nninfctlemfo  12476  ialgr0  12481  algrp1  12483  ennnfonelem0  12891  ennnfonelemp1  12892  ennnfonelemom  12894  ctinfomlemom  12913  nninfdclemp1  12936  ndxarg  12970  strslfv2d  12990  prdsidlem  13394  prdsinvlem  13555  ringidvalg  13838  lidlvalg  14348  rspvalg  14349  znf1o  14528  mplnegfi  14582  upxp  14859  cnmetdval  15116  remetdval  15134  reeflog  15450  nninfnfiinf  16162