Theorem fveq1 5553

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 4031	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5237	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5262	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5262	. 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 4029   iotacio 5213   ` cfv 5254

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 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  fveq1i  5555  fveq1d  5556  fvmptdf  5645  fvmptdv2  5647  isoeq1  5844  oveq  5924  offval  6138  ofrfval  6139  offval3  6186  uchoice  6190  smoeq  6343  recseq  6359  tfr0dm  6375  tfrlemiex  6384  tfr1onlemex  6400  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemex  6413  tfrcllemaccex  6414  tfrcllemres  6415  rdgeq1  6424  rdgivallem  6434  rdgon  6439  rdg0  6440  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  mapsncnv  6749  elixp2  6756  elixpsn  6789  mapsnen  6865  mapxpen  6904  ac6sfi  6954  updjud  7141  nninff  7181  nninfninc  7182  infnninf  7183  infnninfOLD  7184  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  finomni  7199  exmidomni  7201  fodjuomnilemres  7207  ismkvnex  7214  mkvprop  7217  fodjumkvlemres  7218  enmkvlem  7220  enwomnilem  7228  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemg  7234  cc2lem  7326  cc3  7328  1fv  10205  seqeq3  10523  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1olemp  10586  shftvalg  10980  shftval4g  10981  clim  11424  summodc  11526  fsum3  11530  prodmodc  11721  fprodseq  11726  ennnfonelemim  12581  ctinfom  12585  strnfvnd  12638  ptex  12875  prdsex  12880  imasex  12888  xpsff1o  12932  ismhm  13033  isgrpinv  13126  isghm  13313  iscnp  14367  upxp  14440  elcncf  14728  ivthreinc  14799  reldvg  14833  elply2  14881  elplyr  14886  bj-charfunbi  15303  subctctexmid  15491  0nninf  15494  nnsf  15495  peano4nninf  15496  peano3nninf  15497  nninfalllem1  15498  nninfself  15503  nninfsellemeq  15504  nninfsellemeqinf  15506  isomninnlem  15520  trilpolemlt1  15531  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551