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

Theorem atelch 29728
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 29727 . 2 HAtoms ⊆ C
21sseli 3794 1 (𝐴 ∈ HAtoms → 𝐴C )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157   C cch 28311  HAtomscat 28347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-in 3776  df-ss 3783  df-at 29722
This theorem is referenced by:  atsseq  29731  atcveq0  29732  chcv1  29739  chcv2  29740  hatomistici  29746  chrelati  29748  chrelat2i  29749  cvati  29750  cvexchlem  29752  cvp  29759  atnemeq0  29761  atcv0eq  29763  atcv1  29764  atexch  29765  atomli  29766  atoml2i  29767  atordi  29768  atcvatlem  29769  atcvati  29770  atcvat2i  29771  chirredlem1  29774  chirredlem2  29775  chirredlem3  29776  chirredlem4  29777  chirredi  29778  atcvat3i  29780  atcvat4i  29781  atdmd  29782  atmd  29783  atmd2  29784  atabsi  29785  mdsymlem2  29788  mdsymlem3  29789  mdsymlem5  29791  mdsymlem8  29794  atdmd2  29798  sumdmdi  29804  dmdbr4ati  29805  dmdbr5ati  29806  dmdbr6ati  29807
  Copyright terms: Public domain W3C validator