Theorem fveq1i 5640

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

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  11398  resqrexlemf1  11573  resqrexlemfp1  11574  cbvsum  11925  fisumss  11958  fsumadd  11972  isumclim3  11989  cbvprod  12124  fprodssdc  12156  nninfctlemfo  12616  ialgr0  12621  algrp1  12623  ennnfonelem0  13031  ennnfonelemp1  13032  ennnfonelemom  13034  ctinfomlemom  13053  nninfdclemp1  13076  ndxarg  13110  strslfv2d  13130  prdsidlem  13535  prdsinvlem  13696  ringidvalg  13980  lidlvalg  14491  rspvalg  14492  znf1o  14671  mplnegfi  14725  upxp  15002  cnmetdval  15259  remetdval  15277  reeflog  15593  ushgredgedg  16083  ushgredgedgloop  16085  subgruhgredgdm  16127  vtxdumgrfival  16155  vtxd0nedgbfi  16156  vtxduspgrfvedgfi  16158  wlk1walkdom  16216  wlkres  16236  depindlem1  16351  nninfnfiinf  16651