Theorem fveq1 5372

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 3895	. . 3 |- ( F = G -> ( A F x <-> A G x ) )
2	1	iotabidv 5065	. 2 |- ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3		df-fv 5087	. 2 |- ( F ` A ) = ( iota x A F x )
4		df-fv 5087	. 2 |- ( G ` A ) = ( iota x A G x )
5	2, 3, 4	3eqtr4g 2170	1 |- ( F = G -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1312   class class class wbr 3893   iotacio 5042   ` cfv 5079

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-uni 3701  df-br 3894  df-iota 5044  df-fv 5087

This theorem is referenced by:  fveq1i  5374  fveq1d  5375  fvmptdf  5460  fvmptdv2  5462  isoeq1  5654  oveq  5732  offval  5941  ofrfval  5942  offval3  5983  smoeq  6138  recseq  6154  tfr0dm  6170  tfrlemiex  6179  tfr1onlemex  6195  tfr1onlemaccex  6196  tfrcllemsucaccv  6202  tfrcllembxssdm  6204  tfrcllemex  6208  tfrcllemaccex  6209  tfrcllemres  6210  rdgeq1  6219  rdgivallem  6229  rdgon  6234  rdg0  6235  frec0g  6245  freccllem  6250  frecfcllem  6252  frecsuclem  6254  frecsuc  6255  mapsncnv  6540  elixp2  6547  elixpsn  6580  mapsnen  6656  mapxpen  6692  ac6sfi  6742  updjud  6916  enomnilem  6957  finomni  6959  exmidomni  6961  fodjuomnilemres  6967  infnninf  6969  nnnninf  6970  mkvprop  6978  fodjumkvlemres  6979  1fv  9802  seqeq3  10109  iseqf1olemjpcl  10154  iseqf1olemqpcl  10155  iseqf1olemfvp  10156  seq3f1olemqsum  10159  seq3f1olemstep  10160  seq3f1olemp  10161  shftvalg  10494  shftval4g  10495  clim  10935  summodc  11037  fsum3  11041  ennnfonelemim  11775  ctinfom  11779  strnfvnd  11815  iscnp  12203  upxp  12276  elcncf  12539  reldvg  12596  0nninf  12874  nninff  12875  nnsf  12876  peano4nninf  12877  peano3nninf  12878  nninfalllemn  12879  nninfalllem1  12880  nninfself  12886  nninfsellemeq  12887  nninfsellemeqinf  12889  isomninnlem  12902  trilpolemlt1  12911