Theorem atelch 32419

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

Syntax hints:   → wi 4   ∈ wcel 2113   C_ℋ cch 31004  HAtomscat 31040

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-at 32413

This theorem is referenced by:  atsseq  32422  atcveq0  32423  chcv1  32430  chcv2  32431  hatomistici  32437  chrelati  32439  chrelat2i  32440  cvati  32441  cvexchlem  32443  cvp  32450  atnemeq0  32452  atcv0eq  32454  atcv1  32455  atexch  32456  atomli  32457  atoml2i  32458  atordi  32459  atcvatlem  32460  atcvati  32461  atcvat2i  32462  chirredlem1  32465  chirredlem2  32466  chirredlem3  32467  chirredlem4  32468  chirredi  32469  atcvat3i  32471  atcvat4i  32472  atdmd  32473  atmd  32474  atmd2  32475  atabsi  32476  mdsymlem2  32479  mdsymlem3  32480  mdsymlem5  32482  mdsymlem8  32485  atdmd2  32489  sumdmdi  32495  dmdbr4ati  32496  dmdbr5ati  32497  dmdbr6ati  32498