Theorem atelch 30127

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

Step	Hyp	Ref	Expression
1		atssch 30126	. 2 ⊢ HAtoms ⊆ Cℋ
2	1	sseli 3911	1 ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )

Syntax hints:   → wi 4   ∈ wcel 2111   C_ℋ cch 28712  HAtomscat 28748

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-at 30121

This theorem is referenced by:  atsseq  30130  atcveq0  30131  chcv1  30138  chcv2  30139  hatomistici  30145  chrelati  30147  chrelat2i  30148  cvati  30149  cvexchlem  30151  cvp  30158  atnemeq0  30160  atcv0eq  30162  atcv1  30163  atexch  30164  atomli  30165  atoml2i  30166  atordi  30167  atcvatlem  30168  atcvati  30169  atcvat2i  30170  chirredlem1  30173  chirredlem2  30174  chirredlem3  30175  chirredlem4  30176  chirredi  30177  atcvat3i  30179  atcvat4i  30180  atdmd  30181  atmd  30182  atmd2  30183  atabsi  30184  mdsymlem2  30187  mdsymlem3  30188  mdsymlem5  30190  mdsymlem8  30193  atdmd2  30197  sumdmdi  30203  dmdbr4ati  30204  dmdbr5ati  30205  dmdbr6ati  30206