Theorem fveq1 5560

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq1	⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Proof of Theorem fveq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq 4036	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5242	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5267	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5267	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034  ℩cio 5218  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq1i  5562  fveq1d  5563  fvmptdf  5652  fvmptdv2  5654  isoeq1  5851  oveq  5931  offval  6147  ofrfval  6148  offval3  6200  uchoice  6204  smoeq  6357  recseq  6373  tfr0dm  6389  tfrlemiex  6398  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  rdgeq1  6438  rdgivallem  6448  rdgon  6453  rdg0  6454  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  mapsncnv  6763  elixp2  6770  elixpsn  6803  mapsnen  6879  mapxpen  6918  ac6sfi  6968  updjud  7157  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  cc2lem  7349  cc3  7351  1fv  10231  seqeq3  10561  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1olemp  10624  shftvalg  11018  shftval4g  11019  clim  11463  summodc  11565  fsum3  11569  prodmodc  11760  fprodseq  11765  ennnfonelemim  12666  ctinfom  12670  strnfvnd  12723  ptex  12966  prdsex  12971  prdsplusgval  12985  prdsmulrval  12987  imasex  13007  xpsff1o  13051  ismhm  13163  isgrpinv  13256  isghm  13449  iscnp  14519  upxp  14592  elcncf  14893  ivthreinc  14965  reldvg  14999  elply2  15055  elplyr  15060  bj-charfunbi  15541  subctctexmid  15731  0nninf  15735  nnsf  15736  peano4nninf  15737  peano3nninf  15738  nninfalllem1  15739  nninfself  15744  nninfsellemeq  15745  nninfsellemeqinf  15747  isomninnlem  15761  trilpolemlt1  15772  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  dceqnconst  15791  dcapnconst  15792