Theorem fveq1 5230

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq1	|- ( F = G -> ( F ` A ) = ( G ` A ) )

Proof of Theorem fveq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq 3808	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 4939	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 4961	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 4961	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2140	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1285   class class class wbr 3806   iotacio 4916   ` cfv 4953

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-uni 3623  df-br 3807  df-iota 4918  df-fv 4961

This theorem is referenced by:  fveq1i  5232  fveq1d  5233  fvmptdf  5312  fvmptdv2  5314  isoeq1  5494  oveq  5571  offval  5772  ofrfval  5773  offval3  5814  smoeq  5961  recseq  5977  tfr0dm  5993  tfrlemiex  6002  tfr1onlemex  6018  tfr1onlemaccex  6019  tfrcllemsucaccv  6025  tfrcllembxssdm  6027  tfrcllemex  6031  tfrcllemaccex  6032  tfrcllemres  6033  rdgeq1  6042  rdgivallem  6052  rdgon  6057  rdg0  6058  frec0g  6068  freccllem  6073  frecfcllem  6075  frecsuclem  6077  frecsuc  6078  ac6sfi  6456  updjud  6577  finomni  6581  exmidomni  6583  1fv  9303  iseqeq3  9603  shftvalg  9950  shftval4g  9951  clim  10346