Theorem fveq1 5533

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 4020	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5218	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5243	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5243	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2247	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1364   class class class wbr 4018  ℩cio 5194  ‘cfv 5235

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243

This theorem is referenced by:  fveq1i  5535  fveq1d  5536  fvmptdf  5624  fvmptdv2  5626  isoeq1  5823  oveq  5902  offval  6114  ofrfval  6115  offval3  6159  smoeq  6315  recseq  6331  tfr0dm  6347  tfrlemiex  6356  tfr1onlemex  6372  tfr1onlemaccex  6373  tfrcllemsucaccv  6379  tfrcllembxssdm  6381  tfrcllemex  6385  tfrcllemaccex  6386  tfrcllemres  6387  rdgeq1  6396  rdgivallem  6406  rdgon  6411  rdg0  6412  frec0g  6422  freccllem  6427  frecfcllem  6429  frecsuclem  6431  frecsuc  6432  mapsncnv  6721  elixp2  6728  elixpsn  6761  mapsnen  6837  mapxpen  6876  ac6sfi  6926  updjud  7111  nninff  7151  infnninf  7152  infnninfOLD  7153  nnnninf  7154  nnnninfeq  7156  nnnninfeq2  7157  enomnilem  7166  finomni  7168  exmidomni  7170  fodjuomnilemres  7176  ismkvnex  7183  mkvprop  7186  fodjumkvlemres  7187  enmkvlem  7189  enwomnilem  7197  nninfdcinf  7199  nninfwlporlem  7201  nninfwlpoimlemg  7203  cc2lem  7295  cc3  7297  1fv  10169  seqeq3  10481  iseqf1olemjpcl  10526  iseqf1olemqpcl  10527  iseqf1olemfvp  10528  seq3f1olemqsum  10531  seq3f1olemstep  10532  seq3f1olemp  10533  shftvalg  10877  shftval4g  10878  clim  11321  summodc  11423  fsum3  11427  prodmodc  11618  fprodseq  11623  ennnfonelemim  12475  ctinfom  12479  strnfvnd  12532  ptex  12769  prdsex  12774  imasex  12782  xpsff1o  12825  ismhm  12913  isgrpinv  12998  isghm  13182  iscnp  14156  upxp  14229  elcncf  14517  reldvg  14605  bj-charfunbi  15021  subctctexmid  15209  0nninf  15212  nnsf  15213  peano4nninf  15214  peano3nninf  15215  nninfalllem1  15216  nninfself  15221  nninfsellemeq  15222  nninfsellemeqinf  15224  isomninnlem  15237  trilpolemlt1  15248  iswomninnlem  15256  iswomni0  15258  ismkvnnlem  15259  dceqnconst  15267  dcapnconst  15268