Theorem atelch 32493

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 32492	. 2 ⊢ HAtoms ⊆ Cℋ
2	1	sseli 3932	1 ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ )

Syntax hints:   → wi 4   ∈ wcel 2141   C_ℋ cch 31078  HAtomscat 31114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3921  df-at 32487

This theorem is referenced by:  atsseq  32496  atcveq0  32497  chcv1  32504  chcv2  32505  hatomistici  32511  chrelati  32513  chrelat2i  32514  cvati  32515  cvexchlem  32517  cvp  32524  atnemeq0  32526  atcv0eq  32528  atcv1  32529  atexch  32530  atomli  32531  atoml2i  32532  atordi  32533  atcvatlem  32534  atcvati  32535  atcvat2i  32536  chirredlem1  32539  chirredlem2  32540  chirredlem3  32541  chirredlem4  32542  chirredi  32543  atcvat3i  32545  atcvat4i  32546  atdmd  32547  atmd  32548  atmd2  32549  atabsi  32550  mdsymlem2  32553  mdsymlem3  32554  mdsymlem5  32556  mdsymlem8  32559  atdmd2  32563  sumdmdi  32569  dmdbr4ati  32570  dmdbr5ati  32571  dmdbr6ati  32572