Theorem fveq1i 5640

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

Syntax hints:   = wceq 1397   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq12i  5645  fvun2  5713  fvopab3ig  5720  fvsnun1  5851  fvsnun2  5852  fvpr1  5858  fvpr2  5859  fvpr1g  5860  fvpr2g  5861  fvtp1g  5862  fvtp2g  5863  fvtp3g  5864  fvtp2  5866  fvtp3  5867  ov  6141  ovigg  6142  ovg  6161  tfr2a  6487  tfrex  6534  frec0g  6563  freccllem  6568  frecsuclem  6572  caseinl  7290  caseinr  7291  ctssdccl  7310  addpiord  7536  mulpiord  7537  fseq1p1m1  10329  frec2uz0d  10662  frec2uzzd  10663  frec2uzsucd  10664  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdg0  10676  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  0tonninf  10703  1tonninf  10704  inftonninf  10705  seq3val  10723  seqvalcd  10724  hashinfom  11041  hashennn  11043  hashfz1  11046  ccat1st1st  11219  cats1fvd  11348  shftidt  11395  resqrexlemf1  11570  resqrexlemfp1  11571  cbvsum  11922  fisumss  11955  fsumadd  11969  isumclim3  11986  cbvprod  12121  fprodssdc  12153  nninfctlemfo  12613  ialgr0  12618  algrp1  12620  ennnfonelem0  13028  ennnfonelemp1  13029  ennnfonelemom  13031  ctinfomlemom  13050  nninfdclemp1  13073  ndxarg  13107  strslfv2d  13127  prdsidlem  13532  prdsinvlem  13693  ringidvalg  13977  lidlvalg  14488  rspvalg  14489  znf1o  14668  mplnegfi  14722  upxp  14999  cnmetdval  15256  remetdval  15274  reeflog  15590  ushgredgedg  16080  ushgredgedgloop  16082  subgruhgredgdm  16124  vtxdumgrfival  16152  vtxd0nedgbfi  16153  vtxduspgrfvedgfi  16155  wlk1walkdom  16213  wlkres  16233  depindlem1  16346  nninfnfiinf  16646