Theorem atelch 32319

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

Syntax hints:   → wi 4   ∈ wcel 2111   C_ℋ cch 30904  HAtomscat 30940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919  df-at 32313

This theorem is referenced by:  atsseq  32322  atcveq0  32323  chcv1  32330  chcv2  32331  hatomistici  32337  chrelati  32339  chrelat2i  32340  cvati  32341  cvexchlem  32343  cvp  32350  atnemeq0  32352  atcv0eq  32354  atcv1  32355  atexch  32356  atomli  32357  atoml2i  32358  atordi  32359  atcvatlem  32360  atcvati  32361  atcvat2i  32362  chirredlem1  32365  chirredlem2  32366  chirredlem3  32367  chirredlem4  32368  chirredi  32369  atcvat3i  32371  atcvat4i  32372  atdmd  32373  atmd  32374  atmd2  32375  atabsi  32376  mdsymlem2  32379  mdsymlem3  32380  mdsymlem5  32382  mdsymlem8  32385  atdmd2  32389  sumdmdi  32395  dmdbr4ati  32396  dmdbr5ati  32397  dmdbr6ati  32398