Theorem atelch 30706

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

Syntax hints:   → wi 4   ∈ wcel 2106   C_ℋ cch 29291  HAtomscat 29327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-at 30700

This theorem is referenced by:  atsseq  30709  atcveq0  30710  chcv1  30717  chcv2  30718  hatomistici  30724  chrelati  30726  chrelat2i  30727  cvati  30728  cvexchlem  30730  cvp  30737  atnemeq0  30739  atcv0eq  30741  atcv1  30742  atexch  30743  atomli  30744  atoml2i  30745  atordi  30746  atcvatlem  30747  atcvati  30748  atcvat2i  30749  chirredlem1  30752  chirredlem2  30753  chirredlem3  30754  chirredlem4  30755  chirredi  30756  atcvat3i  30758  atcvat4i  30759  atdmd  30760  atmd  30761  atmd2  30762  atabsi  30763  mdsymlem2  30766  mdsymlem3  30767  mdsymlem5  30769  mdsymlem8  30772  atdmd2  30776  sumdmdi  30782  dmdbr4ati  30783  dmdbr5ati  30784  dmdbr6ati  30785