Theorem fveq1i 5676

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

Syntax hints:   = wceq 1398  ‘cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  fveq12i  5681  fvun2  5749  fvopab3ig  5756  fvsnun1  5886  fvsnun2  5887  fvpr1  5893  fvpr2  5894  fvpr1g  5895  fvpr2g  5896  fvtp1g  5897  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  ov  6181  ovigg  6182  ovg  6201  suppsnopdc  6463  tfr2a  6565  tfrex  6612  frec0g  6641  freccllem  6646  frecsuclem  6650  caseinl  7395  caseinr  7396  ctssdccl  7415  addpiord  7647  mulpiord  7648  fseq1p1m1  10453  frec2uz0d  10788  frec2uzzd  10789  frec2uzsucd  10790  frecuzrdgrrn  10797  frec2uzrdg  10798  frecuzrdg0  10802  frecuzrdgsuc  10803  frecuzrdgg  10805  frecuzrdg0t  10811  frecuzrdgsuctlem  10812  0tonninf  10829  1tonninf  10830  inftonninf  10831  seq3val  10849  seqvalcd  10850  hashinfom  11169  hashennn  11171  hashfz1  11174  ccat1st1st  11357  cats1fvd  11486  shftidt  11546  resqrexlemf1  11722  resqrexlemfp1  11723  cbvsum  12074  fisumss  12107  fsumadd  12121  isumclim3  12138  cbvprod  12273  fprodssdc  12305  nninfctlemfo  12765  ialgr0  12770  algrp1  12772  ennnfonelem0  13244  ennnfonelemp1  13245  ennnfonelemom  13247  ctinfomlemom  13266  nninfdclemp1  13289  ndxarg  13323  strslfv2d  13343  prdsidlem  14139  prdsinvlem  14142  ringidvalg  14208  lidlvalg  14749  rspvalg  14750  znf1o  14929  mplnegfi  14990  upxp  15267  cnmetdval  15524  remetdval  15542  reeflog  15858  ushgredgedg  16351  ushgredgedgloop  16353  subgruhgredgdm  16395  vtxdumgrfival  16423  vtxd0nedgbfi  16424  vtxduspgrfvedgfi  16426  wlk1walkdom  16484  wlkres  16504  depindlem1  16631  nninfnfiinf  16941