Theorem fveq1 5588

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 4053	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5263	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5288	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5288	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2264	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4051  ℩cio 5239  ‘cfv 5280

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288

This theorem is referenced by:  fveq1i  5590  fveq1d  5591  fvmptdf  5680  fvmptdv2  5682  isoeq1  5883  oveq  5963  offval  6179  ofrfval  6180  offval3  6232  uchoice  6236  smoeq  6389  recseq  6405  tfr0dm  6421  tfrlemiex  6430  tfr1onlemex  6446  tfr1onlemaccex  6447  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllemex  6459  tfrcllemaccex  6460  tfrcllemres  6461  rdgeq1  6470  rdgivallem  6480  rdgon  6485  rdg0  6486  frec0g  6496  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  mapsncnv  6795  elixp2  6802  elixpsn  6835  mapsnen  6917  mapxpen  6960  ac6sfi  7010  updjud  7199  nninff  7239  nninfninc  7240  infnninf  7241  infnninfOLD  7242  nnnninf  7243  nnnninfeq  7245  nnnninfeq2  7246  enomnilem  7255  finomni  7257  exmidomni  7259  fodjuomnilemres  7265  ismkvnex  7272  mkvprop  7275  fodjumkvlemres  7276  enmkvlem  7278  enwomnilem  7286  nninfdcinf  7288  nninfwlporlem  7290  nninfwlpoimlemg  7292  cc2lem  7398  cc3  7400  1fv  10281  seqeq3  10619  iseqf1olemjpcl  10675  iseqf1olemqpcl  10676  iseqf1olemfvp  10677  seq3f1olemqsum  10680  seq3f1olemstep  10681  seq3f1olemp  10682  ccatfvalfi  11071  wrdl1s1  11107  ccat1st1st  11116  shftvalg  11222  shftval4g  11223  clim  11667  summodc  11769  fsum3  11773  prodmodc  11964  fprodseq  11969  ennnfonelemim  12870  ctinfom  12874  strnfvnd  12927  ptex  13171  prdsex  13176  prdsplusgval  13190  prdsmulrval  13192  imasex  13212  xpsff1o  13256  ismhm  13368  isgrpinv  13461  isghm  13654  mplelbascoe  14529  mplsubgfilemm  14535  mplsubgfilemcl  14536  iscnp  14746  upxp  14819  elcncf  15120  ivthreinc  15192  reldvg  15226  elply2  15282  elplyr  15287  bj-charfunbi  15885  subctctexmid  16078  0nninf  16082  nnsf  16083  peano4nninf  16084  peano3nninf  16085  nninfalllem1  16086  nninfself  16091  nninfsellemeq  16092  nninfsellemeqinf  16094  isomninnlem  16110  trilpolemlt1  16121  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132  dceqnconst  16140  dcapnconst  16141