Theorem fveq1i 5562

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

Syntax hints:   = wceq 1364  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq12i  5567  fvun2  5631  fvopab3ig  5638  fvsnun1  5762  fvsnun2  5763  fvpr1  5769  fvpr2  5770  fvpr1g  5771  fvpr2g  5772  fvtp1g  5773  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  ov  6046  ovigg  6047  ovg  6066  tfr2a  6388  tfrex  6435  frec0g  6464  freccllem  6469  frecsuclem  6473  caseinl  7166  caseinr  7167  ctssdccl  7186  addpiord  7402  mulpiord  7403  fseq1p1m1  10188  frec2uz0d  10510  frec2uzzd  10511  frec2uzsucd  10512  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdg0  10524  frecuzrdgsuc  10525  frecuzrdgg  10527  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  0tonninf  10551  1tonninf  10552  inftonninf  10553  seq3val  10571  seqvalcd  10572  hashinfom  10889  hashennn  10891  hashfz1  10894  shftidt  11017  resqrexlemf1  11192  resqrexlemfp1  11193  cbvsum  11544  fisumss  11576  fsumadd  11590  isumclim3  11607  cbvprod  11742  fprodssdc  11774  nninfctlemfo  12234  ialgr0  12239  algrp1  12241  ennnfonelem0  12649  ennnfonelemp1  12650  ennnfonelemom  12652  ctinfomlemom  12671  nninfdclemp1  12694  ndxarg  12728  strslfv2d  12748  prdsidlem  13151  prdsinvlem  13312  ringidvalg  13595  lidlvalg  14105  rspvalg  14106  znf1o  14285  mplnegfi  14339  upxp  14616  cnmetdval  14873  remetdval  14891  reeflog  15207  nninfnfiinf  15778