Theorem fveq1 5628

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 4085	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5301	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5326	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5326	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2287	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083   iotacio 5276   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq1i  5630  fveq1d  5631  fvmptdf  5724  fvmptdv2  5726  isoeq1  5931  oveq  6013  offval  6232  ofrfval  6233  offval3  6285  uchoice  6289  smoeq  6442  recseq  6458  tfr0dm  6474  tfrlemiex  6483  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  rdgeq1  6523  rdgivallem  6533  rdgon  6538  rdg0  6539  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  mapsncnv  6850  elixp2  6857  elixpsn  6890  mapsnen  6972  mapxpen  7017  ac6sfi  7068  updjud  7260  nninff  7300  nninfninc  7301  infnninf  7302  infnninfOLD  7303  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  cc2lem  7463  cc3  7465  1fv  10347  seqeq3  10686  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  ccatfvalfi  11140  wrdl1s1  11178  ccat1st1st  11188  shftvalg  11363  shftval4g  11364  clim  11808  summodc  11910  fsum3  11914  prodmodc  12105  fprodseq  12110  ennnfonelemim  13011  ctinfom  13015  strnfvnd  13068  ptex  13313  prdsex  13318  prdsplusgval  13332  prdsmulrval  13334  imasex  13354  xpsff1o  13398  ismhm  13510  isgrpinv  13603  isghm  13796  mplelbascoe  14672  mplsubgfilemm  14678  mplsubgfilemcl  14679  iscnp  14889  upxp  14962  elcncf  15263  ivthreinc  15335  reldvg  15369  elply2  15425  elplyr  15430  vtxdgfval  16048  iswlk  16069  uspgr2wlkeq2  16112  isclwwlk  16137  clwwlkn1loopb  16162  bj-charfunbi  16257  subctctexmid  16453  0nninf  16458  nnsf  16459  peano4nninf  16460  peano3nninf  16461  nninfalllem1  16462  nninfself  16467  nninfsellemeq  16468  nninfsellemeqinf  16470  isomninnlem  16486  trilpolemlt1  16497  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508  dceqnconst  16516  dcapnconst  16517