Theorem fveq1 5574

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 4045	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5253	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5278	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5278	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2262	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043  ℩cio 5229  ‘cfv 5270

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278

This theorem is referenced by:  fveq1i  5576  fveq1d  5577  fvmptdf  5666  fvmptdv2  5668  isoeq1  5869  oveq  5949  offval  6165  ofrfval  6166  offval3  6218  uchoice  6222  smoeq  6375  recseq  6391  tfr0dm  6407  tfrlemiex  6416  tfr1onlemex  6432  tfr1onlemaccex  6433  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemex  6445  tfrcllemaccex  6446  tfrcllemres  6447  rdgeq1  6456  rdgivallem  6466  rdgon  6471  rdg0  6472  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  mapsncnv  6781  elixp2  6788  elixpsn  6821  mapsnen  6902  mapxpen  6944  ac6sfi  6994  updjud  7183  nninff  7223  nninfninc  7224  infnninf  7225  infnninfOLD  7226  nnnninf  7227  nnnninfeq  7229  nnnninfeq2  7230  enomnilem  7239  finomni  7241  exmidomni  7243  fodjuomnilemres  7249  ismkvnex  7256  mkvprop  7259  fodjumkvlemres  7260  enmkvlem  7262  enwomnilem  7270  nninfdcinf  7272  nninfwlporlem  7274  nninfwlpoimlemg  7276  cc2lem  7377  cc3  7379  1fv  10260  seqeq3  10595  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  iseqf1olemfvp  10653  seq3f1olemqsum  10656  seq3f1olemstep  10657  seq3f1olemp  10658  ccatfvalfi  11046  wrdl1s1  11082  ccat1st1st  11091  shftvalg  11118  shftval4g  11119  clim  11563  summodc  11665  fsum3  11669  prodmodc  11860  fprodseq  11865  ennnfonelemim  12766  ctinfom  12770  strnfvnd  12823  ptex  13067  prdsex  13072  prdsplusgval  13086  prdsmulrval  13088  imasex  13108  xpsff1o  13152  ismhm  13264  isgrpinv  13357  isghm  13550  mplelbascoe  14425  mplsubgfilemm  14431  mplsubgfilemcl  14432  iscnp  14642  upxp  14715  elcncf  15016  ivthreinc  15088  reldvg  15122  elply2  15178  elplyr  15183  bj-charfunbi  15709  subctctexmid  15899  0nninf  15903  nnsf  15904  peano4nninf  15905  peano3nninf  15906  nninfalllem1  15907  nninfself  15912  nninfsellemeq  15913  nninfsellemeqinf  15915  isomninnlem  15931  trilpolemlt1  15942  iswomninnlem  15950  iswomni0  15952  ismkvnnlem  15953  dceqnconst  15961  dcapnconst  15962