Theorem fveq1 5560

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 4036	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5242	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5267	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5267	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2254	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4034  ℩cio 5218  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267

This theorem is referenced by:  fveq1i  5562  fveq1d  5563  fvmptdf  5652  fvmptdv2  5654  isoeq1  5851  oveq  5931  offval  6147  ofrfval  6148  offval3  6200  uchoice  6204  smoeq  6357  recseq  6373  tfr0dm  6389  tfrlemiex  6398  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  rdgeq1  6438  rdgivallem  6448  rdgon  6453  rdg0  6454  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  mapsncnv  6763  elixp2  6770  elixpsn  6803  mapsnen  6879  mapxpen  6918  ac6sfi  6968  updjud  7157  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  cc2lem  7351  cc3  7353  1fv  10233  seqeq3  10563  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  iseqf1olemfvp  10621  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1olemp  10626  shftvalg  11020  shftval4g  11021  clim  11465  summodc  11567  fsum3  11571  prodmodc  11762  fprodseq  11767  ennnfonelemim  12668  ctinfom  12672  strnfvnd  12725  ptex  12968  prdsex  12973  prdsplusgval  12987  prdsmulrval  12989  imasex  13009  xpsff1o  13053  ismhm  13165  isgrpinv  13258  isghm  13451  mplelbascoe  14326  mplsubgfilemm  14332  mplsubgfilemcl  14333  iscnp  14543  upxp  14616  elcncf  14917  ivthreinc  14989  reldvg  15023  elply2  15079  elplyr  15084  bj-charfunbi  15565  subctctexmid  15755  0nninf  15759  nnsf  15760  peano4nninf  15761  peano3nninf  15762  nninfalllem1  15763  nninfself  15768  nninfsellemeq  15769  nninfsellemeqinf  15771  isomninnlem  15787  trilpolemlt1  15798  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809  dceqnconst  15817  dcapnconst  15818