Theorem fveq1 5495

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 3991	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5181	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5206	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5206	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2228	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1348   class class class wbr 3989  ℩cio 5158  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206

This theorem is referenced by:  fveq1i  5497  fveq1d  5498  fvmptdf  5583  fvmptdv2  5585  isoeq1  5780  oveq  5859  offval  6068  ofrfval  6069  offval3  6113  smoeq  6269  recseq  6285  tfr0dm  6301  tfrlemiex  6310  tfr1onlemex  6326  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemex  6339  tfrcllemaccex  6340  tfrcllemres  6341  rdgeq1  6350  rdgivallem  6360  rdgon  6365  rdg0  6366  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  mapsncnv  6673  elixp2  6680  elixpsn  6713  mapsnen  6789  mapxpen  6826  ac6sfi  6876  updjud  7059  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  finomni  7116  exmidomni  7118  fodjuomnilemres  7124  ismkvnex  7131  mkvprop  7134  fodjumkvlemres  7135  enmkvlem  7137  enwomnilem  7145  nninfdcinf  7147  nninfwlporlem  7149  nninfwlpoimlemg  7151  cc2lem  7228  cc3  7230  1fv  10095  seqeq3  10406  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1olemp  10458  shftvalg  10800  shftval4g  10801  clim  11244  summodc  11346  fsum3  11350  prodmodc  11541  fprodseq  11546  ennnfonelemim  12379  ctinfom  12383  strnfvnd  12436  ismhm  12685  isgrpinv  12756  iscnp  12993  upxp  13066  elcncf  13354  reldvg  13442  bj-charfunbi  13846  subctctexmid  14034  0nninf  14037  nnsf  14038  peano4nninf  14039  peano3nninf  14040  nninfalllem1  14041  nninfself  14046  nninfsellemeq  14047  nninfsellemeqinf  14049  isomninnlem  14062  trilpolemlt1  14073  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092