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

Theorem atelch 32274
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 32273 . 2 HAtoms ⊆ C
21sseli 3974 1 (𝐴 ∈ HAtoms → 𝐴C )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099   C cch 30859  HAtomscat 30895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-ss 3963  df-at 32268
This theorem is referenced by:  atsseq  32277  atcveq0  32278  chcv1  32285  chcv2  32286  hatomistici  32292  chrelati  32294  chrelat2i  32295  cvati  32296  cvexchlem  32298  cvp  32305  atnemeq0  32307  atcv0eq  32309  atcv1  32310  atexch  32311  atomli  32312  atoml2i  32313  atordi  32314  atcvatlem  32315  atcvati  32316  atcvat2i  32317  chirredlem1  32320  chirredlem2  32321  chirredlem3  32322  chirredlem4  32323  chirredi  32324  atcvat3i  32326  atcvat4i  32327  atdmd  32328  atmd  32329  atmd2  32330  atabsi  32331  mdsymlem2  32334  mdsymlem3  32335  mdsymlem5  32337  mdsymlem8  32340  atdmd2  32344  sumdmdi  32350  dmdbr4ati  32351  dmdbr5ati  32352  dmdbr6ati  32353
  Copyright terms: Public domain W3C validator