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

Theorem atelch 31172
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 31171 . 2 HAtoms ⊆ C
21sseli 3938 1 (𝐴 ∈ HAtoms → 𝐴C )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106   C cch 29757  HAtomscat 29793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-in 3915  df-ss 3925  df-at 31166
This theorem is referenced by:  atsseq  31175  atcveq0  31176  chcv1  31183  chcv2  31184  hatomistici  31190  chrelati  31192  chrelat2i  31193  cvati  31194  cvexchlem  31196  cvp  31203  atnemeq0  31205  atcv0eq  31207  atcv1  31208  atexch  31209  atomli  31210  atoml2i  31211  atordi  31212  atcvatlem  31213  atcvati  31214  atcvat2i  31215  chirredlem1  31218  chirredlem2  31219  chirredlem3  31220  chirredlem4  31221  chirredi  31222  atcvat3i  31224  atcvat4i  31225  atdmd  31226  atmd  31227  atmd2  31228  atabsi  31229  mdsymlem2  31232  mdsymlem3  31233  mdsymlem5  31235  mdsymlem8  31238  atdmd2  31242  sumdmdi  31248  dmdbr4ati  31249  dmdbr5ati  31250  dmdbr6ati  31251
  Copyright terms: Public domain W3C validator