Theorem fveq1 5485

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 3984	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5174	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5196	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5196	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2224	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1343   class class class wbr 3982   iotacio 5151   ` cfv 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196

This theorem is referenced by:  fveq1i  5487  fveq1d  5488  fvmptdf  5573  fvmptdv2  5575  isoeq1  5769  oveq  5848  offval  6057  ofrfval  6058  offval3  6102  smoeq  6258  recseq  6274  tfr0dm  6290  tfrlemiex  6299  tfr1onlemex  6315  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemex  6328  tfrcllemaccex  6329  tfrcllemres  6330  rdgeq1  6339  rdgivallem  6349  rdgon  6354  rdg0  6355  frec0g  6365  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  mapsncnv  6661  elixp2  6668  elixpsn  6701  mapsnen  6777  mapxpen  6814  ac6sfi  6864  updjud  7047  nninff  7087  infnninf  7088  infnninfOLD  7089  nnnninf  7090  nnnninfeq  7092  nnnninfeq2  7093  enomnilem  7102  finomni  7104  exmidomni  7106  fodjuomnilemres  7112  ismkvnex  7119  mkvprop  7122  fodjumkvlemres  7123  enmkvlem  7125  enwomnilem  7133  cc2lem  7207  cc3  7209  1fv  10074  seqeq3  10385  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1olemp  10437  shftvalg  10778  shftval4g  10779  clim  11222  summodc  11324  fsum3  11328  prodmodc  11519  fprodseq  11524  ennnfonelemim  12357  ctinfom  12361  strnfvnd  12414  iscnp  12839  upxp  12912  elcncf  13200  reldvg  13288  bj-charfunbi  13693  subctctexmid  13881  0nninf  13884  nnsf  13885  peano4nninf  13886  peano3nninf  13887  nninfalllem1  13888  nninfself  13893  nninfsellemeq  13894  nninfsellemeqinf  13896  isomninnlem  13909  trilpolemlt1  13920  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931  dceqnconst  13938  dcapnconst  13939