Theorem fveq1 5514

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 4005	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5199	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5224	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5224	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2235	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4003   iotacio 5176   ` cfv 5216

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  fveq1i  5516  fveq1d  5517  fvmptdf  5603  fvmptdv2  5605  isoeq1  5801  oveq  5880  offval  6089  ofrfval  6090  offval3  6134  smoeq  6290  recseq  6306  tfr0dm  6322  tfrlemiex  6331  tfr1onlemex  6347  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemex  6360  tfrcllemaccex  6361  tfrcllemres  6362  rdgeq1  6371  rdgivallem  6381  rdgon  6386  rdg0  6387  frec0g  6397  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  mapsncnv  6694  elixp2  6701  elixpsn  6734  mapsnen  6810  mapxpen  6847  ac6sfi  6897  updjud  7080  nninff  7120  infnninf  7121  infnninfOLD  7122  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  finomni  7137  exmidomni  7139  fodjuomnilemres  7145  ismkvnex  7152  mkvprop  7155  fodjumkvlemres  7156  enmkvlem  7158  enwomnilem  7166  nninfdcinf  7168  nninfwlporlem  7170  nninfwlpoimlemg  7172  cc2lem  7264  cc3  7266  1fv  10138  seqeq3  10449  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  iseqf1olemfvp  10496  seq3f1olemqsum  10499  seq3f1olemstep  10500  seq3f1olemp  10501  shftvalg  10844  shftval4g  10845  clim  11288  summodc  11390  fsum3  11394  prodmodc  11585  fprodseq  11590  ennnfonelemim  12424  ctinfom  12428  strnfvnd  12481  ptex  12712  prdsex  12717  imasex  12725  xpsff1o  12767  ismhm  12852  isgrpinv  12925  iscnp  13669  upxp  13742  elcncf  14030  reldvg  14118  bj-charfunbi  14533  subctctexmid  14720  0nninf  14723  nnsf  14724  peano4nninf  14725  peano3nninf  14726  nninfalllem1  14727  nninfself  14732  nninfsellemeq  14733  nninfsellemeqinf  14735  isomninnlem  14748  trilpolemlt1  14759  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770  dceqnconst  14777  dcapnconst  14778