Theorem fveq1i 5560

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

Syntax hints:   = wceq 1364   ` cfv 5259

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq12i  5565  fvun2  5629  fvopab3ig  5636  fvsnun1  5760  fvsnun2  5761  fvpr1  5767  fvpr2  5768  fvpr1g  5769  fvpr2g  5770  fvtp1g  5771  fvtp2g  5772  fvtp3g  5773  fvtp2  5775  fvtp3  5776  ov  6043  ovigg  6044  ovg  6063  tfr2a  6380  tfrex  6427  frec0g  6456  freccllem  6461  frecsuclem  6465  caseinl  7158  caseinr  7159  ctssdccl  7178  addpiord  7385  mulpiord  7386  fseq1p1m1  10171  frec2uz0d  10493  frec2uzzd  10494  frec2uzsucd  10495  frecuzrdgrrn  10502  frec2uzrdg  10503  frecuzrdg0  10507  frecuzrdgsuc  10508  frecuzrdgg  10510  frecuzrdg0t  10516  frecuzrdgsuctlem  10517  0tonninf  10534  1tonninf  10535  inftonninf  10536  seq3val  10554  seqvalcd  10555  hashinfom  10872  hashennn  10874  hashfz1  10877  shftidt  11000  resqrexlemf1  11175  resqrexlemfp1  11176  cbvsum  11527  fisumss  11559  fsumadd  11573  isumclim3  11590  cbvprod  11725  fprodssdc  11757  nninfctlemfo  12217  ialgr0  12222  algrp1  12224  ennnfonelem0  12632  ennnfonelemp1  12633  ennnfonelemom  12635  ctinfomlemom  12654  nninfdclemp1  12677  ndxarg  12711  strslfv2d  12731  ringidvalg  13527  lidlvalg  14037  rspvalg  14038  znf1o  14217  upxp  14518  cnmetdval  14775  remetdval  14793  reeflog  15109