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  5941  oveq  6023  offval  6242  ofrfval  6243  offval3  6295  uchoice  6299  smoeq  6455  recseq  6471  tfr0dm  6487  tfrlemiex  6496  tfr1onlemex  6512  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  rdgeq1  6536  rdgivallem  6546  rdgon  6551  rdg0  6552  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  mapsncnv  6863  elixp2  6870  elixpsn  6903  mapsnen  6985  mapxpen  7033  ac6sfi  7086  updjud  7280  nninff  7320  nninfninc  7321  infnninf  7322  infnninfOLD  7323  nnnninf  7324  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  finomni  7338  exmidomni  7340  fodjuomnilemres  7346  ismkvnex  7353  mkvprop  7356  fodjumkvlemres  7357  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemg  7373  cc2lem  7484  cc3  7486  1fv  10373  seqeq3  10713  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  iseqf1olemfvp  10771  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1olemp  10776  ccatfvalfi  11168  wrdl1s1  11206  ccat1st1st  11217  shftvalg  11396  shftval4g  11397  clim  11841  summodc  11943  fsum3  11947  prodmodc  12138  fprodseq  12143  ennnfonelemim  13044  ctinfom  13048  strnfvnd  13101  ptex  13346  prdsex  13351  prdsplusgval  13365  prdsmulrval  13367  imasex  13387  xpsff1o  13431  ismhm  13543  isgrpinv  13636  isghm  13829  mplelbascoe  14705  mplsubgfilemm  14711  mplsubgfilemcl  14712  iscnp  14922  upxp  14995  elcncf  15296  ivthreinc  15368  reldvg  15402  elply2  15458  elplyr  15463  vtxdgfval  16138  iswlk  16173  uspgr2wlkeq2  16216  isclwwlk  16244  clwwlkn1loopb  16270  clwwlknon  16279  isclwwlknon  16280  s2elclwwlknon2  16286  bj-charfunbi  16406  subctctexmid  16601  0nninf  16606  nnsf  16607  peano4nninf  16608  peano3nninf  16609  nninfalllem1  16610  nninfself  16615  nninfsellemeq  16616  nninfsellemeqinf  16618  isomninnlem  16634  trilpolemlt1  16645  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665