Theorem fveq1i 5696

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 5694	. 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 5377

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 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12i  5701  fvun2  5770  fvopab3ig  5779  fvsnun1  5912  fvsnun2  5913  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvpr2g  5922  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  ov  6208  ovigg  6209  ovg  6228  suppsnopdc  6490  tfr2a  6592  tfrex  6639  frec0g  6668  freccllem  6673  frecsuclem  6677  caseinl  7431  caseinr  7432  ctssdccl  7451  addpiord  7683  mulpiord  7684  fseq1p1m1  10511  frec2uz0d  10849  frec2uzzd  10850  frec2uzsucd  10851  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdg0  10863  frecuzrdgsuc  10864  frecuzrdgg  10866  frecuzrdg0t  10872  frecuzrdgsuctlem  10873  0tonninf  10890  1tonninf  10891  inftonninf  10892  seq3val  10910  seqvalcd  10911  hashinfom  11231  hashennn  11233  hashfz1  11236  ccat1st1st  11423  cats1fvd  11552  shftidt  11612  resqrexlemf1  11788  resqrexlemfp1  11789  cbvsum  12142  fisumss  12175  fsumadd  12189  isumclim3  12206  cbvprod  12341  fprodssdc  12373  nninfctlemfo  12833  ialgr0  12838  algrp1  12840  ennnfonelem0  13345  ennnfonelemp1  13346  ennnfonelemom  13348  ctinfomlemom  13367  nninfdclemp1  13390  ndxarg  13424  strslfv2d  13444  gsumconstcmn  14215  prdsidlem  14242  prdsinvlem  14245  ringidvalg  14313  lidlvalg  14857  rspvalg  14858  znf1o  15035  mplnegfi  15145  upxp  15422  cnmetdval  15679  remetdval  15697  reeflog  16014  logfac  16048  ushgredgedg  16565  ushgredgedgloop  16567  subgruhgredgdm  16609  vtxdumgrfival  16637  vtxd0nedgbfi  16638  vtxduspgrfvedgfi  16640  wlk1walkdom  16698  wlkres  16718  depindlem1  16845  nninfnfiinf  17164