Theorem fveq1 5575

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 4046	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5254	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5279	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5279	. 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 4044   iotacio 5230   ` cfv 5271

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 4045  df-iota 5232  df-fv 5279

This theorem is referenced by:  fveq1i  5577  fveq1d  5578  fvmptdf  5667  fvmptdv2  5669  isoeq1  5870  oveq  5950  offval  6166  ofrfval  6167  offval3  6219  uchoice  6223  smoeq  6376  recseq  6392  tfr0dm  6408  tfrlemiex  6417  tfr1onlemex  6433  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemex  6446  tfrcllemaccex  6447  tfrcllemres  6448  rdgeq1  6457  rdgivallem  6467  rdgon  6472  rdg0  6473  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  mapsncnv  6782  elixp2  6789  elixpsn  6822  mapsnen  6903  mapxpen  6945  ac6sfi  6995  updjud  7184  nninff  7224  nninfninc  7225  infnninf  7226  infnninfOLD  7227  nnnninf  7228  nnnninfeq  7230  nnnninfeq2  7231  enomnilem  7240  finomni  7242  exmidomni  7244  fodjuomnilemres  7250  ismkvnex  7257  mkvprop  7260  fodjumkvlemres  7261  enmkvlem  7263  enwomnilem  7271  nninfdcinf  7273  nninfwlporlem  7275  nninfwlpoimlemg  7277  cc2lem  7378  cc3  7380  1fv  10261  seqeq3  10597  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  iseqf1olemfvp  10655  seq3f1olemqsum  10658  seq3f1olemstep  10659  seq3f1olemp  10660  ccatfvalfi  11048  wrdl1s1  11084  ccat1st1st  11093  shftvalg  11147  shftval4g  11148  clim  11592  summodc  11694  fsum3  11698  prodmodc  11889  fprodseq  11894  ennnfonelemim  12795  ctinfom  12799  strnfvnd  12852  ptex  13096  prdsex  13101  prdsplusgval  13115  prdsmulrval  13117  imasex  13137  xpsff1o  13181  ismhm  13293  isgrpinv  13386  isghm  13579  mplelbascoe  14454  mplsubgfilemm  14460  mplsubgfilemcl  14461  iscnp  14671  upxp  14744  elcncf  15045  ivthreinc  15117  reldvg  15151  elply2  15207  elplyr  15212  bj-charfunbi  15747  subctctexmid  15937  0nninf  15941  nnsf  15942  peano4nninf  15943  peano3nninf  15944  nninfalllem1  15945  nninfself  15950  nninfsellemeq  15951  nninfsellemeqinf  15953  isomninnlem  15969  trilpolemlt1  15980  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991  dceqnconst  15999  dcapnconst  16000