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  7423  nninff  7463  nninfninc  7464  infnninf  7465  infnninfOLD  7466  nnnninf  7467  nnnninfeq  7469  nnnninfeq2  7470  enomnilem  7479  finomni  7481  exmidomni  7483  fodjuomnilemres  7489  ismkvnex  7496  mkvprop  7499  fodjumkvlemres  7500  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemg  7516  cc2lem  7633  cc3  7635  1fv  10557  seqeq3  10904  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1olemp  10967  ccatfvalfi  11376  wrdl1s1  11414  ccat1st1st  11425  shftvalg  11617  shftval4g  11618  clim  12066  summodc  12169  fsum3  12173  prodmodc  12364  fprodseq  12369  ennnfonelemim  13367  ctinfom  13371  strnfvnd  13424  ptex  13671  imasex  13679  xpsff1o  13723  ismhm  13821  isgrpinv  13912  isghm  14099  prdsex  14256  prdsplusgval  14267  prdsmulrval  14269  psrmulfval  15159  mplelbascoe  15174  mplsubgfilemm  15180  mplsubgfilemcl  15181  iscnp  15391  upxp  15464  elcncf  15765  ivthreinc  15837  reldvg  15871  elply2  15927  elplyr  15932  vtxdgfval  16695  iswlk  16730  uspgr2wlkeq2  16773  isclwwlk  16801  clwwlkn1loopb  16827  clwwlknon  16836  isclwwlknon  16837  s2elclwwlknon2  16843  depindlem1  16913  depind  16916  bj-charfunbi  17003  subctctexmid  17196  0nninf  17213  nnsf  17214  peano4nninf  17215  peano3nninf  17216  nninfalllem1  17217  nninfself  17222  nninfsellemeq  17223  nninfsellemeqinf  17225  isomninnlem  17245  trilpolemlt1  17257  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278