Theorem fveq1 5647

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 4095	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5316	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5341	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5341	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2289	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4093   iotacio 5291   ` cfv 5333

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341

This theorem is referenced by:  fveq1i  5649  fveq1d  5650  fvmptdf  5743  fvmptdv2  5745  isoeq1  5952  oveq  6034  offval  6252  ofrfval  6253  offval3  6305  uchoice  6309  smoeq  6499  recseq  6515  tfr0dm  6531  tfrlemiex  6540  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  rdgeq1  6580  rdgivallem  6590  rdgon  6595  rdg0  6596  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  mapsncnv  6907  elixp2  6914  elixpsn  6947  mapsnen  7029  mapxpen  7077  ac6sfi  7130  updjud  7341  nninff  7381  nninfninc  7382  infnninf  7383  infnninfOLD  7384  nnnninf  7385  nnnninfeq  7387  nnnninfeq2  7388  enomnilem  7397  finomni  7399  exmidomni  7401  fodjuomnilemres  7407  ismkvnex  7414  mkvprop  7417  fodjumkvlemres  7418  enmkvlem  7420  enwomnilem  7428  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemg  7434  cc2lem  7545  cc3  7547  1fv  10436  seqeq3  10777  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsum  10838  seq3f1olemstep  10839  seq3f1olemp  10840  ccatfvalfi  11235  wrdl1s1  11273  ccat1st1st  11284  shftvalg  11476  shftval4g  11477  clim  11921  summodc  12024  fsum3  12028  prodmodc  12219  fprodseq  12224  ennnfonelemim  13125  ctinfom  13129  strnfvnd  13182  ptex  13427  prdsex  13432  prdsplusgval  13446  prdsmulrval  13448  imasex  13468  xpsff1o  13512  ismhm  13624  isgrpinv  13717  isghm  13910  mplelbascoe  14793  mplsubgfilemm  14799  mplsubgfilemcl  14800  iscnp  15010  upxp  15083  elcncf  15384  ivthreinc  15456  reldvg  15490  elply2  15546  elplyr  15551  vtxdgfval  16229  iswlk  16264  uspgr2wlkeq2  16307  isclwwlk  16335  clwwlkn1loopb  16361  clwwlknon  16370  isclwwlknon  16371  s2elclwwlknon2  16377  depindlem1  16447  depind  16450  bj-charfunbi  16527  subctctexmid  16722  0nninf  16730  nnsf  16731  peano4nninf  16732  peano3nninf  16733  nninfalllem1  16734  nninfself  16739  nninfsellemeq  16740  nninfsellemeqinf  16742  isomninnlem  16762  trilpolemlt1  16773  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  dceqnconst  16793  dcapnconst  16794