Theorem fveq1i 5636

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fveq1i	⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fveq1 5634	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1395  ‘cfv 5324

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  fveq12i  5641  fvun2  5709  fvopab3ig  5716  fvsnun1  5846  fvsnun2  5847  fvpr1  5853  fvpr2  5854  fvpr1g  5855  fvpr2g  5856  fvtp1g  5857  fvtp2g  5858  fvtp3g  5859  fvtp2  5861  fvtp3  5862  ov  6136  ovigg  6137  ovg  6156  tfr2a  6482  tfrex  6529  frec0g  6558  freccllem  6563  frecsuclem  6567  caseinl  7281  caseinr  7282  ctssdccl  7301  addpiord  7526  mulpiord  7527  fseq1p1m1  10319  frec2uz0d  10651  frec2uzzd  10652  frec2uzsucd  10653  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdg0  10665  frecuzrdgsuc  10666  frecuzrdgg  10668  frecuzrdg0t  10674  frecuzrdgsuctlem  10675  0tonninf  10692  1tonninf  10693  inftonninf  10694  seq3val  10712  seqvalcd  10713  hashinfom  11030  hashennn  11032  hashfz1  11035  ccat1st1st  11208  cats1fvd  11337  shftidt  11384  resqrexlemf1  11559  resqrexlemfp1  11560  cbvsum  11911  fisumss  11943  fsumadd  11957  isumclim3  11974  cbvprod  12109  fprodssdc  12141  nninfctlemfo  12601  ialgr0  12606  algrp1  12608  ennnfonelem0  13016  ennnfonelemp1  13017  ennnfonelemom  13019  ctinfomlemom  13038  nninfdclemp1  13061  ndxarg  13095  strslfv2d  13115  prdsidlem  13520  prdsinvlem  13681  ringidvalg  13964  lidlvalg  14475  rspvalg  14476  znf1o  14655  mplnegfi  14709  upxp  14986  cnmetdval  15243  remetdval  15261  reeflog  15577  ushgredgedg  16065  ushgredgedgloop  16067  vtxdumgrfival  16104  vtxd0nedgbfi  16105  vtxduspgrfvedgfi  16107  wlk1walkdom  16156  wlkres  16174  nninfnfiinf  16561