Theorem fveq1 5554

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 4032	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5238	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5263	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5263	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2251	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4030   iotacio 5214   ` cfv 5255

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  fveq1i  5556  fveq1d  5557  fvmptdf  5646  fvmptdv2  5648  isoeq1  5845  oveq  5925  offval  6140  ofrfval  6141  offval3  6188  uchoice  6192  smoeq  6345  recseq  6361  tfr0dm  6377  tfrlemiex  6386  tfr1onlemex  6402  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemex  6415  tfrcllemaccex  6416  tfrcllemres  6417  rdgeq1  6426  rdgivallem  6436  rdgon  6441  rdg0  6442  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  mapsncnv  6751  elixp2  6758  elixpsn  6791  mapsnen  6867  mapxpen  6906  ac6sfi  6956  updjud  7143  nninff  7183  nninfninc  7184  infnninf  7185  infnninfOLD  7186  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  finomni  7201  exmidomni  7203  fodjuomnilemres  7209  ismkvnex  7216  mkvprop  7219  fodjumkvlemres  7220  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemg  7236  cc2lem  7328  cc3  7330  1fv  10208  seqeq3  10526  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1olemp  10589  shftvalg  10983  shftval4g  10984  clim  11427  summodc  11529  fsum3  11533  prodmodc  11724  fprodseq  11729  ennnfonelemim  12584  ctinfom  12588  strnfvnd  12641  ptex  12878  prdsex  12883  imasex  12891  xpsff1o  12935  ismhm  13036  isgrpinv  13129  isghm  13316  iscnp  14378  upxp  14451  elcncf  14752  ivthreinc  14824  reldvg  14858  elply2  14914  elplyr  14919  bj-charfunbi  15373  subctctexmid  15561  0nninf  15564  nnsf  15565  peano4nninf  15566  peano3nninf  15567  nninfalllem1  15568  nninfself  15573  nninfsellemeq  15574  nninfsellemeqinf  15576  isomninnlem  15590  trilpolemlt1  15601  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621