Theorem fveq1 5697

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 4133	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5363	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5388	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5388	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2296	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   class class class wbr 4131   iotacio 5338   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq1i  5699  fveq1d  5700  fvmptdf  5796  fvmptdv2  5798  isoeq1  6010  oveq  6094  ofovex  6311  offval  6314  ofrfval  6315  offval3  6371  uchoice  6375  smoeq  6565  recseq  6581  tfr0dm  6597  tfrlemiex  6606  tfr1onlemex  6622  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  rdgeq1  6646  rdgivallem  6656  rdgon  6661  rdg0  6662  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  mapsncnv  6981  elixp2  6988  elixpsn  7021  mapsnend  7103  mapsnen  7104  mapxpen  7152  ac6sfi  7206  updjud  7428  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  cc2lem  7638  cc3  7640  1fv  10563  seqeq3  10910  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  ccatfvalfi  11382  wrdl1s1  11420  ccat1st1st  11431  shftvalg  11623  shftval4g  11624  clim  12072  summodc  12175  fsum3  12179  prodmodc  12370  fprodseq  12375  ennnfonelemim  13373  ctinfom  13377  strnfvnd  13430  ptex  13677  imasex  13685  xpsff1o  13729  ismhm  13827  isgrpinv  13918  isghm  14105  prdsex  14279  prdsplusgval  14290  prdsmulrval  14292  psrmulfval  15187  mplelbascoe  15208  mplsubgfilemm  15214  mplsubgfilemcl  15215  iscnp  15425  upxp  15498  elcncf  15799  ivthreinc  15871  reldvg  15905  elply2  15961  elplyr  15966  vtxdgfval  16734  iswlk  16769  uspgr2wlkeq2  16812  isclwwlk  16840  clwwlkn1loopb  16866  clwwlknon  16875  isclwwlknon  16876  s2elclwwlknon2  16882  depindlem1  16952  depind  16955  bj-charfunbi  17042  subctctexmid  17235  0nninf  17253  nnsf  17254  peano4nninf  17255  peano3nninf  17256  nninfalllem1  17257  nninfself  17262  nninfsellemeq  17263  nninfsellemeqinf  17265  isomninnlem  17285  trilpolemlt1  17297  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318