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  10501  frec2uz0d  10836  frec2uzzd  10837  frec2uzsucd  10838  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdg0  10850  frecuzrdgsuc  10851  frecuzrdgg  10853  frecuzrdg0t  10859  frecuzrdgsuctlem  10860  0tonninf  10877  1tonninf  10878  inftonninf  10879  seq3val  10897  seqvalcd  10898  hashinfom  11217  hashennn  11219  hashfz1  11222  ccat1st1st  11409  cats1fvd  11538  shftidt  11598  resqrexlemf1  11774  resqrexlemfp1  11775  cbvsum  12126  fisumss  12159  fsumadd  12173  isumclim3  12190  cbvprod  12325  fprodssdc  12357  nninfctlemfo  12817  ialgr0  12822  algrp1  12824  ennnfonelem0  13296  ennnfonelemp1  13297  ennnfonelemom  13299  ctinfomlemom  13318  nninfdclemp1  13341  ndxarg  13375  strslfv2d  13395  gsumconstcmn  14166  prdsidlem  14193  prdsinvlem  14196  ringidvalg  14264  lidlvalg  14808  rspvalg  14809  znf1o  14986  mplnegfi  15096  upxp  15373  cnmetdval  15630  remetdval  15648  reeflog  15964  logfac  15995  ushgredgedg  16467  ushgredgedgloop  16469  subgruhgredgdm  16511  vtxdumgrfival  16539  vtxd0nedgbfi  16540  vtxduspgrfvedgfi  16542  wlk1walkdom  16600  wlkres  16620  depindlem1  16747  nninfnfiinf  17066