Theorem fveq1 5634

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4086  ℩cio 5282  ‘cfv 5324

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 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  fveq1i  5636  fveq1d  5637  fvmptdf  5730  fvmptdv2  5732  isoeq1  5937  oveq  6019  offval  6238  ofrfval  6239  offval3  6291  uchoice  6295  smoeq  6451  recseq  6467  tfr0dm  6483  tfrlemiex  6492  tfr1onlemex  6508  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  rdgeq1  6532  rdgivallem  6542  rdgon  6547  rdg0  6548  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  mapsncnv  6859  elixp2  6866  elixpsn  6899  mapsnen  6981  mapxpen  7029  ac6sfi  7080  updjud  7272  nninff  7312  nninfninc  7313  infnninf  7314  infnninfOLD  7315  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  finomni  7330  exmidomni  7332  fodjuomnilemres  7338  ismkvnex  7345  mkvprop  7348  fodjumkvlemres  7349  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemg  7365  cc2lem  7475  cc3  7477  1fv  10364  seqeq3  10704  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  iseqf1olemfvp  10762  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1olemp  10767  ccatfvalfi  11159  wrdl1s1  11197  ccat1st1st  11208  shftvalg  11387  shftval4g  11388  clim  11832  summodc  11934  fsum3  11938  prodmodc  12129  fprodseq  12134  ennnfonelemim  13035  ctinfom  13039  strnfvnd  13092  ptex  13337  prdsex  13342  prdsplusgval  13356  prdsmulrval  13358  imasex  13378  xpsff1o  13422  ismhm  13534  isgrpinv  13627  isghm  13820  mplelbascoe  14696  mplsubgfilemm  14702  mplsubgfilemcl  14703  iscnp  14913  upxp  14986  elcncf  15287  ivthreinc  15359  reldvg  15393  elply2  15449  elplyr  15454  vtxdgfval  16094  iswlk  16120  uspgr2wlkeq2  16163  isclwwlk  16189  clwwlkn1loopb  16215  clwwlknon  16224  isclwwlknon  16225  s2elclwwlknon2  16231  bj-charfunbi  16342  subctctexmid  16537  0nninf  16542  nnsf  16543  peano4nninf  16544  peano3nninf  16545  nninfalllem1  16546  nninfself  16551  nninfsellemeq  16552  nninfsellemeqinf  16554  isomninnlem  16570  trilpolemlt1  16581  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601