Theorem fveq1 5569

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

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

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 5229  df-fv 5276

This theorem is referenced by:  fveq1i  5571  fveq1d  5572  fvmptdf  5661  fvmptdv2  5663  isoeq1  5860  oveq  5940  offval  6156  ofrfval  6157  offval3  6209  uchoice  6213  smoeq  6366  recseq  6382  tfr0dm  6398  tfrlemiex  6407  tfr1onlemex  6423  tfr1onlemaccex  6424  tfrcllemsucaccv  6430  tfrcllembxssdm  6432  tfrcllemex  6436  tfrcllemaccex  6437  tfrcllemres  6438  rdgeq1  6447  rdgivallem  6457  rdgon  6462  rdg0  6463  frec0g  6473  freccllem  6478  frecfcllem  6480  frecsuclem  6482  frecsuc  6483  mapsncnv  6772  elixp2  6779  elixpsn  6812  mapsnen  6888  mapxpen  6927  ac6sfi  6977  updjud  7166  nninff  7206  nninfninc  7207  infnninf  7208  infnninfOLD  7209  nnnninf  7210  nnnninfeq  7212  nnnninfeq2  7213  enomnilem  7222  finomni  7224  exmidomni  7226  fodjuomnilemres  7232  ismkvnex  7239  mkvprop  7242  fodjumkvlemres  7243  enmkvlem  7245  enwomnilem  7253  nninfdcinf  7255  nninfwlporlem  7257  nninfwlpoimlemg  7259  cc2lem  7360  cc3  7362  1fv  10243  seqeq3  10578  iseqf1olemjpcl  10634  iseqf1olemqpcl  10635  iseqf1olemfvp  10636  seq3f1olemqsum  10639  seq3f1olemstep  10640  seq3f1olemp  10641  ccatfvalfi  11023  shftvalg  11066  shftval4g  11067  clim  11511  summodc  11613  fsum3  11617  prodmodc  11808  fprodseq  11813  ennnfonelemim  12714  ctinfom  12718  strnfvnd  12771  ptex  13014  prdsex  13019  prdsplusgval  13033  prdsmulrval  13035  imasex  13055  xpsff1o  13099  ismhm  13211  isgrpinv  13304  isghm  13497  mplelbascoe  14372  mplsubgfilemm  14378  mplsubgfilemcl  14379  iscnp  14589  upxp  14662  elcncf  14963  ivthreinc  15035  reldvg  15069  elply2  15125  elplyr  15130  bj-charfunbi  15611  subctctexmid  15801  0nninf  15805  nnsf  15806  peano4nninf  15807  peano3nninf  15808  nninfalllem1  15809  nninfself  15814  nninfsellemeq  15815  nninfsellemeqinf  15817  isomninnlem  15833  trilpolemlt1  15844  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855  dceqnconst  15863  dcapnconst  15864