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  11222  cats1fvd  11351  shftidt  11411  resqrexlemf1  11586  resqrexlemfp1  11587  cbvsum  11938  fisumss  11971  fsumadd  11985  isumclim3  12002  cbvprod  12137  fprodssdc  12169  nninfctlemfo  12629  ialgr0  12634  algrp1  12636  ennnfonelem0  13044  ennnfonelemp1  13045  ennnfonelemom  13047  ctinfomlemom  13066  nninfdclemp1  13089  ndxarg  13123  strslfv2d  13143  prdsidlem  13548  prdsinvlem  13709  ringidvalg  13993  lidlvalg  14504  rspvalg  14505  znf1o  14684  mplnegfi  14738  upxp  15015  cnmetdval  15272  remetdval  15290  reeflog  15606  ushgredgedg  16096  ushgredgedgloop  16098  subgruhgredgdm  16140  vtxdumgrfival  16168  vtxd0nedgbfi  16169  vtxduspgrfvedgfi  16171  wlk1walkdom  16229  wlkres  16249  depindlem1  16376  nninfnfiinf  16676