Theorem fveq1 5669

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 4111	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5335	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5360	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5360	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2290	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4109  ℩cio 5310  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  fveq1i  5671  fveq1d  5672  fvmptdf  5765  fvmptdv2  5767  isoeq1  5974  oveq  6056  offval  6274  ofrfval  6275  offval3  6327  uchoice  6331  smoeq  6521  recseq  6537  tfr0dm  6553  tfrlemiex  6562  tfr1onlemex  6578  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemex  6591  tfrcllemaccex  6592  tfrcllemres  6593  rdgeq1  6602  rdgivallem  6612  rdgon  6617  rdg0  6618  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  mapsncnv  6930  elixp2  6937  elixpsn  6970  mapsnend  7052  mapsnen  7053  mapxpen  7101  ac6sfi  7155  updjud  7373  nninff  7413  nninfninc  7414  infnninf  7415  infnninfOLD  7416  nnnninf  7417  nnnninfeq  7419  nnnninfeq2  7420  enomnilem  7429  finomni  7431  exmidomni  7433  fodjuomnilemres  7439  ismkvnex  7446  mkvprop  7449  fodjumkvlemres  7450  enmkvlem  7452  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemg  7466  cc2lem  7580  cc3  7582  1fv  10473  seqeq3  10814  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  iseqf1olemfvp  10872  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1olemp  10877  ccatfvalfi  11280  wrdl1s1  11318  ccat1st1st  11329  shftvalg  11521  shftval4g  11522  clim  11966  summodc  12069  fsum3  12073  prodmodc  12264  fprodseq  12269  ennnfonelemim  13175  ctinfom  13179  strnfvnd  13232  ptex  13477  prdsex  13482  prdsplusgval  13496  prdsmulrval  13498  imasex  13518  xpsff1o  13562  ismhm  13674  isgrpinv  13767  isghm  13960  mplelbascoe  14847  mplsubgfilemm  14853  mplsubgfilemcl  14854  iscnp  15064  upxp  15137  elcncf  15438  ivthreinc  15510  reldvg  15544  elply2  15600  elplyr  15605  vtxdgfval  16283  iswlk  16318  uspgr2wlkeq2  16361  isclwwlk  16389  clwwlkn1loopb  16415  clwwlknon  16424  isclwwlknon  16425  s2elclwwlknon2  16431  depindlem1  16501  depind  16504  bj-charfunbi  16581  subctctexmid  16774  0nninf  16782  nnsf  16783  peano4nninf  16784  peano3nninf  16785  nninfalllem1  16786  nninfself  16791  nninfsellemeq  16792  nninfsellemeqinf  16794  isomninnlem  16814  trilpolemlt1  16825  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847