Theorem fveq1 5638

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 4090	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5309	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5334	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5334	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088  ℩cio 5284  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq1i  5640  fveq1d  5641  fvmptdf  5734  fvmptdv2  5736  isoeq1  5942  oveq  6024  offval  6243  ofrfval  6244  offval3  6296  uchoice  6300  smoeq  6456  recseq  6472  tfr0dm  6488  tfrlemiex  6497  tfr1onlemex  6513  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  rdgeq1  6537  rdgivallem  6547  rdgon  6552  rdg0  6553  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  mapsncnv  6864  elixp2  6871  elixpsn  6904  mapsnen  6986  mapxpen  7034  ac6sfi  7087  updjud  7281  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  finomni  7339  exmidomni  7341  fodjuomnilemres  7347  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  cc2lem  7485  cc3  7487  1fv  10374  seqeq3  10715  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1olemp  10778  ccatfvalfi  11173  wrdl1s1  11211  ccat1st1st  11222  shftvalg  11414  shftval4g  11415  clim  11859  summodc  11962  fsum3  11966  prodmodc  12157  fprodseq  12162  ennnfonelemim  13063  ctinfom  13067  strnfvnd  13120  ptex  13365  prdsex  13370  prdsplusgval  13384  prdsmulrval  13386  imasex  13406  xpsff1o  13450  ismhm  13562  isgrpinv  13655  isghm  13848  mplelbascoe  14725  mplsubgfilemm  14731  mplsubgfilemcl  14732  iscnp  14942  upxp  15015  elcncf  15316  ivthreinc  15388  reldvg  15422  elply2  15478  elplyr  15483  vtxdgfval  16158  iswlk  16193  uspgr2wlkeq2  16236  isclwwlk  16264  clwwlkn1loopb  16290  clwwlknon  16299  isclwwlknon  16300  s2elclwwlknon2  16306  depindlem1  16376  depind  16379  bj-charfunbi  16457  subctctexmid  16652  0nninf  16657  nnsf  16658  peano4nninf  16659  peano3nninf  16660  nninfalllem1  16661  nninfself  16666  nninfsellemeq  16667  nninfsellemeqinf  16669  isomninnlem  16685  trilpolemlt1  16696  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717