Theorem fveq1i 5579

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

Syntax hints:   = wceq 1373   ` cfv 5272

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  fveq12i  5584  fvun2  5648  fvopab3ig  5655  fvsnun1  5783  fvsnun2  5784  fvpr1  5790  fvpr2  5791  fvpr1g  5792  fvpr2g  5793  fvtp1g  5794  fvtp2g  5795  fvtp3g  5796  fvtp2  5798  fvtp3  5799  ov  6067  ovigg  6068  ovg  6087  tfr2a  6409  tfrex  6456  frec0g  6485  freccllem  6490  frecsuclem  6494  caseinl  7195  caseinr  7196  ctssdccl  7215  addpiord  7431  mulpiord  7432  fseq1p1m1  10218  frec2uz0d  10546  frec2uzzd  10547  frec2uzsucd  10548  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdg0  10560  frecuzrdgsuc  10561  frecuzrdgg  10563  frecuzrdg0t  10569  frecuzrdgsuctlem  10570  0tonninf  10587  1tonninf  10588  inftonninf  10589  seq3val  10607  seqvalcd  10608  hashinfom  10925  hashennn  10927  hashfz1  10930  ccat1st1st  11096  shftidt  11177  resqrexlemf1  11352  resqrexlemfp1  11353  cbvsum  11704  fisumss  11736  fsumadd  11750  isumclim3  11767  cbvprod  11902  fprodssdc  11934  nninfctlemfo  12394  ialgr0  12399  algrp1  12401  ennnfonelem0  12809  ennnfonelemp1  12810  ennnfonelemom  12812  ctinfomlemom  12831  nninfdclemp1  12854  ndxarg  12888  strslfv2d  12908  prdsidlem  13312  prdsinvlem  13473  ringidvalg  13756  lidlvalg  14266  rspvalg  14267  znf1o  14446  mplnegfi  14500  upxp  14777  cnmetdval  15034  remetdval  15052  reeflog  15368  nninfnfiinf  15997