Theorem fveq1i 5627

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 5625	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)

Syntax hints:   = wceq 1395  ‘cfv 5317

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 3888  df-br 4083  df-iota 5277  df-fv 5325

This theorem is referenced by:  fveq12i  5632  fvun2  5700  fvopab3ig  5707  fvsnun1  5835  fvsnun2  5836  fvpr1  5842  fvpr2  5843  fvpr1g  5844  fvpr2g  5845  fvtp1g  5846  fvtp2g  5847  fvtp3g  5848  fvtp2  5850  fvtp3  5851  ov  6123  ovigg  6124  ovg  6143  tfr2a  6465  tfrex  6512  frec0g  6541  freccllem  6546  frecsuclem  6550  caseinl  7254  caseinr  7255  ctssdccl  7274  addpiord  7499  mulpiord  7500  fseq1p1m1  10286  frec2uz0d  10616  frec2uzzd  10617  frec2uzsucd  10618  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdg0  10630  frecuzrdgsuc  10631  frecuzrdgg  10633  frecuzrdg0t  10639  frecuzrdgsuctlem  10640  0tonninf  10657  1tonninf  10658  inftonninf  10659  seq3val  10677  seqvalcd  10678  hashinfom  10995  hashennn  10997  hashfz1  11000  ccat1st1st  11167  cats1fvd  11293  shftidt  11339  resqrexlemf1  11514  resqrexlemfp1  11515  cbvsum  11866  fisumss  11898  fsumadd  11912  isumclim3  11929  cbvprod  12064  fprodssdc  12096  nninfctlemfo  12556  ialgr0  12561  algrp1  12563  ennnfonelem0  12971  ennnfonelemp1  12972  ennnfonelemom  12974  ctinfomlemom  12993  nninfdclemp1  13016  ndxarg  13050  strslfv2d  13070  prdsidlem  13475  prdsinvlem  13636  ringidvalg  13919  lidlvalg  14429  rspvalg  14430  znf1o  14609  mplnegfi  14663  upxp  14940  cnmetdval  15197  remetdval  15215  reeflog  15531  ushgredgedg  16018  ushgredgedgloop  16020  nninfnfiinf  16348