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  6597  tfrex  6644  frec0g  6673  freccllem  6678  frecsuclem  6682  caseinl  7437  caseinr  7438  ctssdccl  7457  addpiord  7689  mulpiord  7690  fseq1p1m1  10517  frec2uz0d  10856  frec2uzzd  10857  frec2uzsucd  10858  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdg0  10870  frecuzrdgsuc  10871  frecuzrdgg  10873  frecuzrdg0t  10879  frecuzrdgsuctlem  10880  0tonninf  10897  1tonninf  10898  inftonninf  10899  seq3val  10917  seqvalcd  10918  hashinfom  11238  hashennn  11240  hashfz1  11243  ccat1st1st  11430  cats1fvd  11559  shftidt  11619  resqrexlemf1  11795  resqrexlemfp1  11796  cbvsum  12150  fisumss  12183  fsumadd  12197  isumclim3  12214  cbvprod  12349  fprodssdc  12381  nninfctlemfo  12841  ialgr0  12846  algrp1  12848  ennnfonelem0  13353  ennnfonelemp1  13354  ennnfonelemom  13356  ctinfomlemom  13375  nninfdclemp1  13398  ndxarg  13432  strslfv2d  13452  gsumconstcmn  14265  prdsidlem  14299  prdsinvlem  14302  ringidvalg  14370  lidlvalg  14916  rspvalg  14917  znf1o  15094  mplnegfi  15238  upxp  15515  cnmetdval  15772  remetdval  15790  reeflog  16109  logfac  16143  ushgredgedg  16689  ushgredgedgloop  16691  subgruhgredgdm  16733  vtxdumgrfival  16761  vtxd0nedgbfi  16762  vtxduspgrfvedgfi  16764  wlk1walkdom  16822  wlkres  16842  depindlem1  16969  nninfnfiinf  17289