Theorem fveq1 5317

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 3853	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5014	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5036	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5036	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2146	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1290   class class class wbr 3851  ℩cio 4991  ‘cfv 5028

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rex 2366  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036

This theorem is referenced by:  fveq1i  5319  fveq1d  5320  fvmptdf  5403  fvmptdv2  5405  isoeq1  5594  oveq  5672  offval  5877  ofrfval  5878  offval3  5919  smoeq  6069  recseq  6085  tfr0dm  6101  tfrlemiex  6110  tfr1onlemex  6126  tfr1onlemaccex  6127  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllemex  6139  tfrcllemaccex  6140  tfrcllemres  6141  rdgeq1  6150  rdgivallem  6160  rdgon  6165  rdg0  6166  frec0g  6176  freccllem  6181  frecfcllem  6183  frecsuclem  6185  frecsuc  6186  mapsncnv  6466  elixp2  6473  elixpsn  6506  mapsnen  6582  mapxpen  6618  ac6sfi  6668  updjud  6827  enomnilem  6855  finomni  6857  exmidomni  6859  fodjuomnilemres  6864  infnninf  6866  nnnninf  6867  1fv  9611  iseqeq3  9921  iseqf1olemjpcl  9985  iseqf1olemqpcl  9986  iseqf1olemfvp  9987  seq3f1olemqsum  9990  seq3f1olemstep  9991  seq3f1olemp  9992  shftvalg  10331  shftval4g  10332  clim  10730  isummo  10834  fisum  10839  strnfvnd  11575  elcncf  11902  0nninf  12165  nninff  12166  nnsf  12167  peano4nninf  12168  peano3nninf  12169  nninfalllemn  12170  nninfalllem1  12171  nninfself  12177  nninfsellemeq  12178  nninfsellemeqinf  12180