Theorem fveq1 5516

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 4007	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5201	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5226	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5226	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2235	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 4005  ℩cio 5178  ‘cfv 5218

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226

This theorem is referenced by:  fveq1i  5518  fveq1d  5519  fvmptdf  5605  fvmptdv2  5607  isoeq1  5804  oveq  5883  offval  6092  ofrfval  6093  offval3  6137  smoeq  6293  recseq  6309  tfr0dm  6325  tfrlemiex  6334  tfr1onlemex  6350  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemex  6363  tfrcllemaccex  6364  tfrcllemres  6365  rdgeq1  6374  rdgivallem  6384  rdgon  6389  rdg0  6390  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  mapsncnv  6697  elixp2  6704  elixpsn  6737  mapsnen  6813  mapxpen  6850  ac6sfi  6900  updjud  7083  nninff  7123  infnninf  7124  infnninfOLD  7125  nnnninf  7126  nnnninfeq  7128  nnnninfeq2  7129  enomnilem  7138  finomni  7140  exmidomni  7142  fodjuomnilemres  7148  ismkvnex  7155  mkvprop  7158  fodjumkvlemres  7159  enmkvlem  7161  enwomnilem  7169  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemg  7175  cc2lem  7267  cc3  7269  1fv  10141  seqeq3  10452  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsum  10502  seq3f1olemstep  10503  seq3f1olemp  10504  shftvalg  10847  shftval4g  10848  clim  11291  summodc  11393  fsum3  11397  prodmodc  11588  fprodseq  11593  ennnfonelemim  12427  ctinfom  12431  strnfvnd  12484  ptex  12718  prdsex  12723  imasex  12731  xpsff1o  12773  ismhm  12858  isgrpinv  12931  iscnp  13738  upxp  13811  elcncf  14099  reldvg  14187  bj-charfunbi  14602  subctctexmid  14789  0nninf  14792  nnsf  14793  peano4nninf  14794  peano3nninf  14795  nninfalllem1  14796  nninfself  14801  nninfsellemeq  14802  nninfsellemeqinf  14804  isomninnlem  14817  trilpolemlt1  14828  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  dceqnconst  14846  dcapnconst  14847