Theorem fveq1 5626

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 4085	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5301	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5326	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5326	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2287	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1395   class class class wbr 4083   iotacio 5276   ` cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq1i  5628  fveq1d  5629  fvmptdf  5722  fvmptdv2  5724  isoeq1  5925  oveq  6007  offval  6226  ofrfval  6227  offval3  6279  uchoice  6283  smoeq  6436  recseq  6452  tfr0dm  6468  tfrlemiex  6477  tfr1onlemex  6493  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemex  6506  tfrcllemaccex  6507  tfrcllemres  6508  rdgeq1  6517  rdgivallem  6527  rdgon  6532  rdg0  6533  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  mapsncnv  6842  elixp2  6849  elixpsn  6882  mapsnen  6964  mapxpen  7009  ac6sfi  7060  updjud  7249  nninff  7289  nninfninc  7290  infnninf  7291  infnninfOLD  7292  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  finomni  7307  exmidomni  7309  fodjuomnilemres  7315  ismkvnex  7322  mkvprop  7325  fodjumkvlemres  7326  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemg  7342  cc2lem  7452  cc3  7454  1fv  10335  seqeq3  10674  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsum  10735  seq3f1olemstep  10736  seq3f1olemp  10737  ccatfvalfi  11127  wrdl1s1  11163  ccat1st1st  11172  shftvalg  11347  shftval4g  11348  clim  11792  summodc  11894  fsum3  11898  prodmodc  12089  fprodseq  12094  ennnfonelemim  12995  ctinfom  12999  strnfvnd  13052  ptex  13297  prdsex  13302  prdsplusgval  13316  prdsmulrval  13318  imasex  13338  xpsff1o  13382  ismhm  13494  isgrpinv  13587  isghm  13780  mplelbascoe  14656  mplsubgfilemm  14662  mplsubgfilemcl  14663  iscnp  14873  upxp  14946  elcncf  15247  ivthreinc  15319  reldvg  15353  elply2  15409  elplyr  15414  iswlk  16036  uspgr2wlkeq2  16077  bj-charfunbi  16174  subctctexmid  16366  0nninf  16370  nnsf  16371  peano4nninf  16372  peano3nninf  16373  nninfalllem1  16374  nninfself  16379  nninfsellemeq  16380  nninfsellemeqinf  16382  isomninnlem  16398  trilpolemlt1  16409  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  dceqnconst  16428  dcapnconst  16429