Theorem fveq1 5515

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 4006	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5200	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5225	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5225	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2235	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4004   iotacio 5177   ` cfv 5217

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225

This theorem is referenced by:  fveq1i  5517  fveq1d  5518  fvmptdf  5604  fvmptdv2  5606  isoeq1  5802  oveq  5881  offval  6090  ofrfval  6091  offval3  6135  smoeq  6291  recseq  6307  tfr0dm  6323  tfrlemiex  6332  tfr1onlemex  6348  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemex  6361  tfrcllemaccex  6362  tfrcllemres  6363  rdgeq1  6372  rdgivallem  6382  rdgon  6387  rdg0  6388  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  mapsncnv  6695  elixp2  6702  elixpsn  6735  mapsnen  6811  mapxpen  6848  ac6sfi  6898  updjud  7081  nninff  7121  infnninf  7122  infnninfOLD  7123  nnnninf  7124  nnnninfeq  7126  nnnninfeq2  7127  enomnilem  7136  finomni  7138  exmidomni  7140  fodjuomnilemres  7146  ismkvnex  7153  mkvprop  7156  fodjumkvlemres  7157  enmkvlem  7159  enwomnilem  7167  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemg  7173  cc2lem  7265  cc3  7267  1fv  10139  seqeq3  10450  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1olemp  10502  shftvalg  10845  shftval4g  10846  clim  11289  summodc  11391  fsum3  11395  prodmodc  11586  fprodseq  11591  ennnfonelemim  12425  ctinfom  12429  strnfvnd  12482  ptex  12713  prdsex  12718  imasex  12726  xpsff1o  12768  ismhm  12853  isgrpinv  12926  iscnp  13702  upxp  13775  elcncf  14063  reldvg  14151  bj-charfunbi  14566  subctctexmid  14753  0nninf  14756  nnsf  14757  peano4nninf  14758  peano3nninf  14759  nninfalllem1  14760  nninfself  14765  nninfsellemeq  14766  nninfsellemeqinf  14768  isomninnlem  14781  trilpolemlt1  14792  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811