Theorem fveq1 5694

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 4132	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5360	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5385	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5385	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4130  ℩cio 5335  ‘cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq1i  5696  fveq1d  5697  fvmptdf  5793  fvmptdv2  5795  isoeq1  6007  oveq  6091  offval  6310  ofrfval  6311  offval3  6367  uchoice  6371  smoeq  6561  recseq  6577  tfr0dm  6593  tfrlemiex  6602  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  rdgeq1  6642  rdgivallem  6652  rdgon  6657  rdg0  6658  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  mapsncnv  6977  elixp2  6984  elixpsn  7017  mapsnend  7099  mapsnen  7100  mapxpen  7148  ac6sfi  7202  updjud  7422  nninff  7462  nninfninc  7463  infnninf  7464  infnninfOLD  7465  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  cc2lem  7632  cc3  7634  1fv  10556  seqeq3  10902  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1olemp  10965  ccatfvalfi  11374  wrdl1s1  11412  ccat1st1st  11423  shftvalg  11615  shftval4g  11616  clim  12063  summodc  12166  fsum3  12170  prodmodc  12361  fprodseq  12366  ennnfonelemim  13364  ctinfom  13368  strnfvnd  13421  ptex  13667  imasex  13675  xpsff1o  13719  ismhm  13817  isgrpinv  13908  isghm  14095  prdsex  14221  prdsplusgval  14232  prdsmulrval  14234  mplelbascoe  15132  mplsubgfilemm  15138  mplsubgfilemcl  15139  iscnp  15349  upxp  15422  elcncf  15723  ivthreinc  15795  reldvg  15829  elply2  15885  elplyr  15890  vtxdgfval  16627  iswlk  16662  uspgr2wlkeq2  16705  isclwwlk  16733  clwwlkn1loopb  16759  clwwlknon  16768  isclwwlknon  16769  s2elclwwlknon2  16775  depindlem1  16845  depind  16848  bj-charfunbi  16935  subctctexmid  17128  0nninf  17145  nnsf  17146  peano4nninf  17147  peano3nninf  17148  nninfalllem1  17149  nninfself  17154  nninfsellemeq  17155  nninfsellemeqinf  17157  isomninnlem  17177  trilpolemlt1  17188  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209