Theorem fveq1 5506

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 4000	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5191	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5216	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5216	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2233	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 3998   iotacio 5168   ` cfv 5208

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216

This theorem is referenced by:  fveq1i  5508  fveq1d  5509  fvmptdf  5595  fvmptdv2  5597  isoeq1  5792  oveq  5871  offval  6080  ofrfval  6081  offval3  6125  smoeq  6281  recseq  6297  tfr0dm  6313  tfrlemiex  6322  tfr1onlemex  6338  tfr1onlemaccex  6339  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllemex  6351  tfrcllemaccex  6352  tfrcllemres  6353  rdgeq1  6362  rdgivallem  6372  rdgon  6377  rdg0  6378  frec0g  6388  freccllem  6393  frecfcllem  6395  frecsuclem  6397  frecsuc  6398  mapsncnv  6685  elixp2  6692  elixpsn  6725  mapsnen  6801  mapxpen  6838  ac6sfi  6888  updjud  7071  nninff  7111  infnninf  7112  infnninfOLD  7113  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  enomnilem  7126  finomni  7128  exmidomni  7130  fodjuomnilemres  7136  ismkvnex  7143  mkvprop  7146  fodjumkvlemres  7147  enmkvlem  7149  enwomnilem  7157  nninfdcinf  7159  nninfwlporlem  7161  nninfwlpoimlemg  7163  cc2lem  7240  cc3  7242  1fv  10109  seqeq3  10420  iseqf1olemjpcl  10465  iseqf1olemqpcl  10466  iseqf1olemfvp  10467  seq3f1olemqsum  10470  seq3f1olemstep  10471  seq3f1olemp  10472  shftvalg  10813  shftval4g  10814  clim  11257  summodc  11359  fsum3  11363  prodmodc  11554  fprodseq  11559  ennnfonelemim  12392  ctinfom  12396  strnfvnd  12449  ismhm  12725  isgrpinv  12797  iscnp  13279  upxp  13352  elcncf  13640  reldvg  13728  bj-charfunbi  14132  subctctexmid  14320  0nninf  14323  nnsf  14324  peano4nninf  14325  peano3nninf  14326  nninfalllem1  14327  nninfself  14332  nninfsellemeq  14333  nninfsellemeqinf  14335  isomninnlem  14348  trilpolemlt1  14359  iswomninnlem  14367  iswomni0  14369  ismkvnnlem  14370  dceqnconst  14377  dcapnconst  14378