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  7400  mulpiord  7401  fseq1p1m1  10186  frec2uz0d  10508  frec2uzzd  10509  frec2uzsucd  10510  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdg0  10522  frecuzrdgsuc  10523  frecuzrdgg  10525  frecuzrdg0t  10531  frecuzrdgsuctlem  10532  0tonninf  10549  1tonninf  10550  inftonninf  10551  seq3val  10569  seqvalcd  10570  hashinfom  10887  hashennn  10889  hashfz1  10892  shftidt  11015  resqrexlemf1  11190  resqrexlemfp1  11191  cbvsum  11542  fisumss  11574  fsumadd  11588  isumclim3  11605  cbvprod  11740  fprodssdc  11772  nninfctlemfo  12232  ialgr0  12237  algrp1  12239  ennnfonelem0  12647  ennnfonelemp1  12648  ennnfonelemom  12650  ctinfomlemom  12669  nninfdclemp1  12692  ndxarg  12726  strslfv2d  12746  prdsidlem  13149  prdsinvlem  13310  ringidvalg  13593  lidlvalg  14103  rspvalg  14104  znf1o  14283  upxp  14592  cnmetdval  14849  remetdval  14867  reeflog  15183