Theorem atelch 31460

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

Syntax hints:   → wi 4   ∈ wcel 2106   C_ℋ cch 30045  HAtomscat 30081

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3951  df-ss 3961  df-at 31454

This theorem is referenced by:  atsseq  31463  atcveq0  31464  chcv1  31471  chcv2  31472  hatomistici  31478  chrelati  31480  chrelat2i  31481  cvati  31482  cvexchlem  31484  cvp  31491  atnemeq0  31493  atcv0eq  31495  atcv1  31496  atexch  31497  atomli  31498  atoml2i  31499  atordi  31500  atcvatlem  31501  atcvati  31502  atcvat2i  31503  chirredlem1  31506  chirredlem2  31507  chirredlem3  31508  chirredlem4  31509  chirredi  31510  atcvat3i  31512  atcvat4i  31513  atdmd  31514  atmd  31515  atmd2  31516  atabsi  31517  mdsymlem2  31520  mdsymlem3  31521  mdsymlem5  31523  mdsymlem8  31526  atdmd2  31530  sumdmdi  31536  dmdbr4ati  31537  dmdbr5ati  31538  dmdbr6ati  31539