Theorem fveq1 5557

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 4035	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5241	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5266	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5266	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2254	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4033   iotacio 5217   ` cfv 5258

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266

This theorem is referenced by:  fveq1i  5559  fveq1d  5560  fvmptdf  5649  fvmptdv2  5651  isoeq1  5848  oveq  5928  offval  6143  ofrfval  6144  offval3  6191  uchoice  6195  smoeq  6348  recseq  6364  tfr0dm  6380  tfrlemiex  6389  tfr1onlemex  6405  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemex  6418  tfrcllemaccex  6419  tfrcllemres  6420  rdgeq1  6429  rdgivallem  6439  rdgon  6444  rdg0  6445  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  mapsncnv  6754  elixp2  6761  elixpsn  6794  mapsnen  6870  mapxpen  6909  ac6sfi  6959  updjud  7148  nninff  7188  nninfninc  7189  infnninf  7190  infnninfOLD  7191  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  enomnilem  7204  finomni  7206  exmidomni  7208  fodjuomnilemres  7214  ismkvnex  7221  mkvprop  7224  fodjumkvlemres  7225  enmkvlem  7227  enwomnilem  7235  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemg  7241  cc2lem  7333  cc3  7335  1fv  10214  seqeq3  10544  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1olemp  10607  shftvalg  11001  shftval4g  11002  clim  11446  summodc  11548  fsum3  11552  prodmodc  11743  fprodseq  11748  ennnfonelemim  12641  ctinfom  12645  strnfvnd  12698  ptex  12935  prdsex  12940  imasex  12948  xpsff1o  12992  ismhm  13093  isgrpinv  13186  isghm  13373  iscnp  14435  upxp  14508  elcncf  14809  ivthreinc  14881  reldvg  14915  elply2  14971  elplyr  14976  bj-charfunbi  15457  subctctexmid  15645  0nninf  15648  nnsf  15649  peano4nninf  15650  peano3nninf  15651  nninfalllem1  15652  nninfself  15657  nninfsellemeq  15658  nninfsellemeqinf  15660  isomninnlem  15674  trilpolemlt1  15685  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  dceqnconst  15704  dcapnconst  15705