Theorem fveq1i 5179

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1i.1	|- F = G

Assertion

Ref	Expression
fveq1i	|- ( F ` A ) = ( G ` A )

Proof of Theorem fveq1i

Step	Hyp	Ref	Expression
1		fveq1i.1	. 2 |- F = G
2		fveq1 5177	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	ax-mp 7	1 |- ( F ` A ) = ( G ` A )

Syntax hints:   = wceq 1243   ` cfv 4902

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910

This theorem is referenced by:  fveq12i  5183  fvun2  5240  fvopab3ig  5246  fvsnun1  5360  fvsnun2  5361  fvpr1  5365  fvpr2  5366  fvpr1g  5367  fvpr2g  5368  fvtp1g  5369  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  ov  5620  ovigg  5621  ovg  5639  tfr2a  5936  tfrex  5954  frec0g  5983  frecsuclem1  5987  frecsuclem2  5989  addpiord  6414  mulpiord  6415  fseq1p1m1  8956  frec2uz0d  9185  frec2uzzd  9186  frec2uzsucd  9187  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdg0  9200  frecuzrdgsuc  9201  shftidt  9434  resqrexlemf1  9606  resqrexlemfp1  9607  ialgr0  9883  ialgrp1  9885