ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fveq1 GIF version

Theorem fveq1 5388
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.
StepHypRef Expression
1 breq 3901 . . 3 (𝐹 = 𝐺 → (𝐴𝐹𝑥𝐴𝐺𝑥))
21iotabidv 5079 . 2 (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3 df-fv 5101 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
4 df-fv 5101 . 2 (𝐺𝐴) = (℩𝑥𝐴𝐺𝑥)
52, 3, 43eqtr4g 2175 1 (𝐹 = 𝐺 → (𝐹𝐴) = (𝐺𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316   class class class wbr 3899  cio 5056  cfv 5093
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101
This theorem is referenced by:  fveq1i  5390  fveq1d  5391  fvmptdf  5476  fvmptdv2  5478  isoeq1  5670  oveq  5748  offval  5957  ofrfval  5958  offval3  6000  smoeq  6155  recseq  6171  tfr0dm  6187  tfrlemiex  6196  tfr1onlemex  6212  tfr1onlemaccex  6213  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllemex  6225  tfrcllemaccex  6226  tfrcllemres  6227  rdgeq1  6236  rdgivallem  6246  rdgon  6251  rdg0  6252  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  mapsncnv  6557  elixp2  6564  elixpsn  6597  mapsnen  6673  mapxpen  6710  ac6sfi  6760  updjud  6935  enomnilem  6978  finomni  6980  exmidomni  6982  fodjuomnilemres  6988  infnninf  6990  nnnninf  6991  ismkvnex  6997  mkvprop  7000  fodjumkvlemres  7001  1fv  9884  seqeq3  10191  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsum  10241  seq3f1olemstep  10242  seq3f1olemp  10243  shftvalg  10576  shftval4g  10577  clim  11018  summodc  11120  fsum3  11124  ennnfonelemim  11864  ctinfom  11868  strnfvnd  11906  iscnp  12295  upxp  12368  elcncf  12656  reldvg  12744  subctctexmid  13123  0nninf  13124  nninff  13125  nnsf  13126  peano4nninf  13127  peano3nninf  13128  nninfalllemn  13129  nninfalllem1  13130  nninfself  13136  nninfsellemeq  13137  nninfsellemeqinf  13139  isomninnlem  13152  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator