Theorem fveq1 5533

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 4020	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5218	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5243	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5243	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2247	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4018   iotacio 5194   ` cfv 5235

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243

This theorem is referenced by:  fveq1i  5535  fveq1d  5536  fvmptdf  5624  fvmptdv2  5626  isoeq1  5823  oveq  5903  offval  6115  ofrfval  6116  offval3  6160  smoeq  6316  recseq  6332  tfr0dm  6348  tfrlemiex  6357  tfr1onlemex  6373  tfr1onlemaccex  6374  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllemex  6386  tfrcllemaccex  6387  tfrcllemres  6388  rdgeq1  6397  rdgivallem  6407  rdgon  6412  rdg0  6413  frec0g  6423  freccllem  6428  frecfcllem  6430  frecsuclem  6432  frecsuc  6433  mapsncnv  6722  elixp2  6729  elixpsn  6762  mapsnen  6838  mapxpen  6877  ac6sfi  6927  updjud  7112  nninff  7152  infnninf  7153  infnninfOLD  7154  nnnninf  7155  nnnninfeq  7157  nnnninfeq2  7158  enomnilem  7167  finomni  7169  exmidomni  7171  fodjuomnilemres  7177  ismkvnex  7184  mkvprop  7187  fodjumkvlemres  7188  enmkvlem  7190  enwomnilem  7198  nninfdcinf  7200  nninfwlporlem  7202  nninfwlpoimlemg  7204  cc2lem  7296  cc3  7298  1fv  10171  seqeq3  10483  iseqf1olemjpcl  10528  iseqf1olemqpcl  10529  iseqf1olemfvp  10530  seq3f1olemqsum  10533  seq3f1olemstep  10534  seq3f1olemp  10535  shftvalg  10880  shftval4g  10881  clim  11324  summodc  11426  fsum3  11430  prodmodc  11621  fprodseq  11626  ennnfonelemim  12478  ctinfom  12482  strnfvnd  12535  ptex  12772  prdsex  12777  imasex  12785  xpsff1o  12828  ismhm  12928  isgrpinv  13013  isghm  13199  iscnp  14176  upxp  14249  elcncf  14537  reldvg  14625  bj-charfunbi  15041  subctctexmid  15229  0nninf  15232  nnsf  15233  peano4nninf  15234  peano3nninf  15235  nninfalllem1  15236  nninfself  15241  nninfsellemeq  15242  nninfsellemeqinf  15244  isomninnlem  15257  trilpolemlt1  15268  iswomninnlem  15276  iswomni0  15278  ismkvnnlem  15279  dceqnconst  15287  dcapnconst  15288