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  10546  seqeq3  10889  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1olemp  10952  ccatfvalfi  11360  wrdl1s1  11398  ccat1st1st  11409  shftvalg  11601  shftval4g  11602  clim  12047  summodc  12150  fsum3  12154  prodmodc  12345  fprodseq  12350  ennnfonelemim  13315  ctinfom  13319  strnfvnd  13372  ptex  13618  imasex  13626  xpsff1o  13670  ismhm  13768  isgrpinv  13859  isghm  14046  prdsex  14172  prdsplusgval  14183  prdsmulrval  14185  mplelbascoe  15083  mplsubgfilemm  15089  mplsubgfilemcl  15090  iscnp  15300  upxp  15373  elcncf  15674  ivthreinc  15746  reldvg  15780  elply2  15836  elplyr  15841  vtxdgfval  16529  iswlk  16564  uspgr2wlkeq2  16607  isclwwlk  16635  clwwlkn1loopb  16661  clwwlknon  16670  isclwwlknon  16671  s2elclwwlknon2  16677  depindlem1  16747  depind  16750  bj-charfunbi  16837  subctctexmid  17030  0nninf  17047  nnsf  17048  peano4nninf  17049  peano3nninf  17050  nninfalllem1  17051  nninfself  17056  nninfsellemeq  17057  nninfsellemeqinf  17059  isomninnlem  17079  trilpolemlt1  17090  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111