Theorem atelch 32440

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

Syntax hints:   → wi 4   ∈ wcel 2119   C_ℋ cch 31025  HAtomscat 31061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-at 32434

This theorem is referenced by:  atsseq  32443  atcveq0  32444  chcv1  32451  chcv2  32452  hatomistici  32458  chrelati  32460  chrelat2i  32461  cvati  32462  cvexchlem  32464  cvp  32471  atnemeq0  32473  atcv0eq  32475  atcv1  32476  atexch  32477  atomli  32478  atoml2i  32479  atordi  32480  atcvatlem  32481  atcvati  32482  atcvat2i  32483  chirredlem1  32486  chirredlem2  32487  chirredlem3  32488  chirredlem4  32489  chirredi  32490  atcvat3i  32492  atcvat4i  32493  atdmd  32494  atmd  32495  atmd2  32496  atabsi  32497  mdsymlem2  32500  mdsymlem3  32501  mdsymlem5  32503  mdsymlem8  32506  atdmd2  32510  sumdmdi  32516  dmdbr4ati  32517  dmdbr5ati  32518  dmdbr6ati  32519