Theorem fveq1 5697

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4131  ℩cio 5338  ‘cfv 5380

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 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq1i  5699  fveq1d  5700  fvmptdf  5796  fvmptdv2  5798  isoeq1  6010  oveq  6094  ofovex  6311  offval  6314  ofrfval  6315  offval3  6371  uchoice  6375  smoeq  6566  recseq  6582  tfr0dm  6598  tfrlemiex  6607  tfr1onlemex  6623  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  rdgeq1  6647  rdgivallem  6657  rdgon  6662  rdg0  6663  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  mapsncnv  6983  elixp2  6990  elixpsn  7023  mapsnend  7105  mapsnen  7106  mapxpen  7154  ac6sfi  7208  updjud  7428  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  cc2lem  7638  cc3  7640  1fv  10562  seqeq3  10909  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1olemp  10972  ccatfvalfi  11381  wrdl1s1  11419  ccat1st1st  11430  shftvalg  11622  shftval4g  11623  clim  12071  summodc  12174  fsum3  12178  prodmodc  12369  fprodseq  12374  ennnfonelemim  13372  ctinfom  13376  strnfvnd  13429  ptex  13676  imasex  13684  xpsff1o  13728  ismhm  13826  isgrpinv  13917  isghm  14104  prdsex  14278  prdsplusgval  14289  prdsmulrval  14291  psrbagmaxlem1  15178  psrbagmax  15183  psrmulfval  15196  iscnp  15442  upxp  15515  elcncf  15816  ivthreinc  15888  reldvg  15922  elply2  15978  elplyr  15983  vtxdgfval  16751  iswlk  16786  uspgr2wlkeq2  16829  isclwwlk  16857  clwwlkn1loopb  16883  clwwlknon  16892  isclwwlknon  16893  s2elclwwlknon2  16899  depindlem1  16969  depind  16972  bj-charfunbi  17059  subctctexmid  17252  0nninf  17270  nnsf  17271  peano4nninf  17272  peano3nninf  17273  nninfalllem1  17274  nninfself  17279  nninfsellemeq  17280  nninfsellemeqinf  17282  isomninnlem  17302  trilpolemlt1  17314  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335