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

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

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