HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  atelch Structured version   Visualization version   GIF version

Theorem atelch 28421
Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
atelch (𝐴 ∈ HAtoms → 𝐴C )

Proof of Theorem atelch
StepHypRef Expression
1 atssch 28420 . 2 HAtoms ⊆ C
21sseli 3563 1 (𝐴 ∈ HAtoms → 𝐴C )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   C cch 27004  HAtomscat 27040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-in 3546  df-ss 3553  df-at 28415
This theorem is referenced by:  atsseq  28424  atcveq0  28425  chcv1  28432  chcv2  28433  hatomistici  28439  chrelati  28441  chrelat2i  28442  cvati  28443  cvexchlem  28445  cvp  28452  atnemeq0  28454  atcv0eq  28456  atcv1  28457  atexch  28458  atomli  28459  atoml2i  28460  atordi  28461  atcvatlem  28462  atcvati  28463  atcvat2i  28464  chirredlem1  28467  chirredlem2  28468  chirredlem3  28469  chirredlem4  28470  chirredi  28471  atcvat3i  28473  atcvat4i  28474  atdmd  28475  atmd  28476  atmd2  28477  atabsi  28478  mdsymlem2  28481  mdsymlem3  28482  mdsymlem5  28484  mdsymlem8  28487  atdmd2  28491  sumdmdi  28497  dmdbr4ati  28498  dmdbr5ati  28499  dmdbr6ati  28500
  Copyright terms: Public domain W3C validator