Theorem fveq1 5506

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 4000	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5191	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5216	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5216	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2233	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 3998  ℩cio 5168  ‘cfv 5208

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216

This theorem is referenced by:  fveq1i  5508  fveq1d  5509  fvmptdf  5595  fvmptdv2  5597  isoeq1  5792  oveq  5871  offval  6080  ofrfval  6081  offval3  6125  smoeq  6281  recseq  6297  tfr0dm  6313  tfrlemiex  6322  tfr1onlemex  6338  tfr1onlemaccex  6339  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllemex  6351  tfrcllemaccex  6352  tfrcllemres  6353  rdgeq1  6362  rdgivallem  6372  rdgon  6377  rdg0  6378  frec0g  6388  freccllem  6393  frecfcllem  6395  frecsuclem  6397  frecsuc  6398  mapsncnv  6685  elixp2  6692  elixpsn  6725  mapsnen  6801  mapxpen  6838  ac6sfi  6888  updjud  7071  nninff  7111  infnninf  7112  infnninfOLD  7113  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  enomnilem  7126  finomni  7128  exmidomni  7130  fodjuomnilemres  7136  ismkvnex  7143  mkvprop  7146  fodjumkvlemres  7147  enmkvlem  7149  enwomnilem  7157  nninfdcinf  7159  nninfwlporlem  7161  nninfwlpoimlemg  7163  cc2lem  7240  cc3  7242  1fv  10107  seqeq3  10418  iseqf1olemjpcl  10463  iseqf1olemqpcl  10464  iseqf1olemfvp  10465  seq3f1olemqsum  10468  seq3f1olemstep  10469  seq3f1olemp  10470  shftvalg  10811  shftval4g  10812  clim  11255  summodc  11357  fsum3  11361  prodmodc  11552  fprodseq  11557  ennnfonelemim  12390  ctinfom  12394  strnfvnd  12447  ismhm  12714  isgrpinv  12786  iscnp  13250  upxp  13323  elcncf  13611  reldvg  13699  bj-charfunbi  14103  subctctexmid  14291  0nninf  14294  nnsf  14295  peano4nninf  14296  peano3nninf  14297  nninfalllem1  14298  nninfself  14303  nninfsellemeq  14304  nninfsellemeqinf  14306  isomninnlem  14319  trilpolemlt1  14330  iswomninnlem  14338  iswomni0  14340  ismkvnnlem  14341  dceqnconst  14348  dcapnconst  14349