Theorem fveq1 5628

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 4085	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5301	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5326	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5326	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4083  ℩cio 5276  ‘cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326

This theorem is referenced by:  fveq1i  5630  fveq1d  5631  fvmptdf  5724  fvmptdv2  5726  isoeq1  5931  oveq  6013  offval  6232  ofrfval  6233  offval3  6285  uchoice  6289  smoeq  6442  recseq  6458  tfr0dm  6474  tfrlemiex  6483  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  rdgeq1  6523  rdgivallem  6533  rdgon  6538  rdg0  6539  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  mapsncnv  6850  elixp2  6857  elixpsn  6890  mapsnen  6972  mapxpen  7017  ac6sfi  7068  updjud  7260  nninff  7300  nninfninc  7301  infnninf  7302  infnninfOLD  7303  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemg  7353  cc2lem  7463  cc3  7465  1fv  10347  seqeq3  10686  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  ccatfvalfi  11140  wrdl1s1  11178  ccat1st1st  11187  shftvalg  11362  shftval4g  11363  clim  11807  summodc  11909  fsum3  11913  prodmodc  12104  fprodseq  12109  ennnfonelemim  13010  ctinfom  13014  strnfvnd  13067  ptex  13312  prdsex  13317  prdsplusgval  13331  prdsmulrval  13333  imasex  13353  xpsff1o  13397  ismhm  13509  isgrpinv  13602  isghm  13795  mplelbascoe  14671  mplsubgfilemm  14677  mplsubgfilemcl  14678  iscnp  14888  upxp  14961  elcncf  15262  ivthreinc  15334  reldvg  15368  elply2  15424  elplyr  15429  vtxdgfval  16047  iswlk  16064  uspgr2wlkeq2  16107  isclwwlk  16132  bj-charfunbi  16229  subctctexmid  16425  0nninf  16430  nnsf  16431  peano4nninf  16432  peano3nninf  16433  nninfalllem1  16434  nninfself  16439  nninfsellemeq  16440  nninfsellemeqinf  16442  isomninnlem  16458  trilpolemlt1  16469  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480  dceqnconst  16488  dcapnconst  16489