Theorem fveq1i 5699

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

This proof depends on syntax axioms:   = wceq 1402   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq12i  5704  fvun2  5773  fvopab3ig  5782  fvsnun1  5915  fvsnun2  5916  fvpr1  5922  fvpr2  5923  fvpr1g  5924  fvpr2g  5925  fvtp1g  5926  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  ov  6211  ovigg  6212  ovg  6231  suppsnopdc  6494  tfr2a  6596  tfrex  6643  frec0g  6672  freccllem  6677  frecsuclem  6681  caseinl  7437  caseinr  7438  ctssdccl  7457  addpiord  7689  mulpiord  7690  fseq1p1m1  10518  frec2uz0d  10857  frec2uzzd  10858  frec2uzsucd  10859  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdg0  10871  frecuzrdgsuc  10872  frecuzrdgg  10874  frecuzrdg0t  10880  frecuzrdgsuctlem  10881  0tonninf  10898  1tonninf  10899  inftonninf  10900  seq3val  10918  seqvalcd  10919  hashinfom  11239  hashennn  11241  hashfz1  11244  ccat1st1st  11431  cats1fvd  11560  shftidt  11620  resqrexlemf1  11796  resqrexlemfp1  11797  cbvsum  12151  fisumss  12184  fsumadd  12198  isumclim3  12215  cbvprod  12350  fprodssdc  12382  nninfctlemfo  12842  ialgr0  12847  algrp1  12849  ennnfonelem0  13354  ennnfonelemp1  13355  ennnfonelemom  13357  ctinfomlemom  13376  nninfdclemp1  13399  ndxarg  13433  strslfv2d  13453  gsumconstcmn  14266  prdsidlem  14300  prdsinvlem  14303  ringidvalg  14371  lidlvalg  14917  rspvalg  14918  znf1o  15095  mplnegfi  15221  upxp  15498  cnmetdval  15755  remetdval  15773  reeflog  16092  logfac  16126  ushgredgedg  16672  ushgredgedgloop  16674  subgruhgredgdm  16716  vtxdumgrfival  16744  vtxd0nedgbfi  16745  vtxduspgrfvedgfi  16747  wlk1walkdom  16805  wlkres  16825  depindlem1  16952  nninfnfiinf  17272