Theorem fveq1 5577

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 4047	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5255	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5280	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5280	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2263	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1373   class class class wbr 4045   iotacio 5231   ` cfv 5272

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  fveq1i  5579  fveq1d  5580  fvmptdf  5669  fvmptdv2  5671  isoeq1  5872  oveq  5952  offval  6168  ofrfval  6169  offval3  6221  uchoice  6225  smoeq  6378  recseq  6394  tfr0dm  6410  tfrlemiex  6419  tfr1onlemex  6435  tfr1onlemaccex  6436  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemex  6448  tfrcllemaccex  6449  tfrcllemres  6450  rdgeq1  6459  rdgivallem  6469  rdgon  6474  rdg0  6475  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  mapsncnv  6784  elixp2  6791  elixpsn  6824  mapsnen  6905  mapxpen  6947  ac6sfi  6997  updjud  7186  nninff  7226  nninfninc  7227  infnninf  7228  infnninfOLD  7229  nnnninf  7230  nnnninfeq  7232  nnnninfeq2  7233  enomnilem  7242  finomni  7244  exmidomni  7246  fodjuomnilemres  7252  ismkvnex  7259  mkvprop  7262  fodjumkvlemres  7263  enmkvlem  7265  enwomnilem  7273  nninfdcinf  7275  nninfwlporlem  7277  nninfwlpoimlemg  7279  cc2lem  7380  cc3  7382  1fv  10263  seqeq3  10599  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsum  10660  seq3f1olemstep  10661  seq3f1olemp  10662  ccatfvalfi  11051  wrdl1s1  11087  ccat1st1st  11096  shftvalg  11180  shftval4g  11181  clim  11625  summodc  11727  fsum3  11731  prodmodc  11922  fprodseq  11927  ennnfonelemim  12828  ctinfom  12832  strnfvnd  12885  ptex  13129  prdsex  13134  prdsplusgval  13148  prdsmulrval  13150  imasex  13170  xpsff1o  13214  ismhm  13326  isgrpinv  13419  isghm  13612  mplelbascoe  14487  mplsubgfilemm  14493  mplsubgfilemcl  14494  iscnp  14704  upxp  14777  elcncf  15078  ivthreinc  15150  reldvg  15184  elply2  15240  elplyr  15245  bj-charfunbi  15784  subctctexmid  15974  0nninf  15978  nnsf  15979  peano4nninf  15980  peano3nninf  15981  nninfalllem1  15982  nninfself  15987  nninfsellemeq  15988  nninfsellemeqinf  15990  isomninnlem  16006  trilpolemlt1  16017  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028  dceqnconst  16036  dcapnconst  16037