Theorem atelch 32674

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

Syntax hints:   → wi 4   ∈ wcel 2143   C_ℋ cch 31259  HAtomscat 31295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923  df-at 32668

This theorem is referenced by:  atsseq  32677  atcveq0  32678  chcv1  32685  chcv2  32686  hatomistici  32692  chrelati  32694  chrelat2i  32695  cvati  32696  cvexchlem  32698  cvp  32705  atnemeq0  32707  atcv0eq  32709  atcv1  32710  atexch  32711  atomli  32712  atoml2i  32713  atordi  32714  atcvatlem  32715  atcvati  32716  atcvat2i  32717  chirredlem1  32720  chirredlem2  32721  chirredlem3  32722  chirredlem4  32723  chirredi  32724  atcvat3i  32726  atcvat4i  32727  atdmd  32728  atmd  32729  atmd2  32730  atabsi  32731  mdsymlem2  32734  mdsymlem3  32735  mdsymlem5  32737  mdsymlem8  32740  atdmd2  32744  sumdmdi  32750  dmdbr4ati  32751  dmdbr5ati  32752  dmdbr6ati  32753