Theorem fveq1i 5696

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

This proof depends on syntax axioms:   = wceq 1402  ‘cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12i  5701  fvun2  5770  fvopab3ig  5779  fvsnun1  5912  fvsnun2  5913  fvpr1  5919  fvpr2  5920  fvpr1g  5921  fvpr2g  5922  fvtp1g  5923  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  ov  6208  ovigg  6209  ovg  6228  suppsnopdc  6490  tfr2a  6592  tfrex  6639  frec0g  6668  freccllem  6673  frecsuclem  6677  caseinl  7432  caseinr  7433  ctssdccl  7452  addpiord  7684  mulpiord  7685  fseq1p1m1  10512  frec2uz0d  10851  frec2uzzd  10852  frec2uzsucd  10853  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdg0  10865  frecuzrdgsuc  10866  frecuzrdgg  10868  frecuzrdg0t  10874  frecuzrdgsuctlem  10875  0tonninf  10892  1tonninf  10893  inftonninf  10894  seq3val  10912  seqvalcd  10913  hashinfom  11233  hashennn  11235  hashfz1  11238  ccat1st1st  11425  cats1fvd  11554  shftidt  11614  resqrexlemf1  11790  resqrexlemfp1  11791  cbvsum  12145  fisumss  12178  fsumadd  12192  isumclim3  12209  cbvprod  12344  fprodssdc  12376  nninfctlemfo  12836  ialgr0  12841  algrp1  12843  ennnfonelem0  13348  ennnfonelemp1  13349  ennnfonelemom  13351  ctinfomlemom  13370  nninfdclemp1  13393  ndxarg  13427  strslfv2d  13447  gsumconstcmn  14250  prdsidlem  14277  prdsinvlem  14280  ringidvalg  14348  lidlvalg  14892  rspvalg  14893  znf1o  15070  mplnegfi  15187  upxp  15464  cnmetdval  15721  remetdval  15739  reeflog  16056  logfac  16090  ushgredgedg  16633  ushgredgedgloop  16635  subgruhgredgdm  16677  vtxdumgrfival  16705  vtxd0nedgbfi  16706  vtxduspgrfvedgfi  16708  wlk1walkdom  16766  wlkres  16786  depindlem1  16913  nninfnfiinf  17232