Theorem atelch 31597

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

Syntax hints:   → wi 4   ∈ wcel 2107   C_ℋ cch 30182  HAtomscat 30218

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-at 31591

This theorem is referenced by:  atsseq  31600  atcveq0  31601  chcv1  31608  chcv2  31609  hatomistici  31615  chrelati  31617  chrelat2i  31618  cvati  31619  cvexchlem  31621  cvp  31628  atnemeq0  31630  atcv0eq  31632  atcv1  31633  atexch  31634  atomli  31635  atoml2i  31636  atordi  31637  atcvatlem  31638  atcvati  31639  atcvat2i  31640  chirredlem1  31643  chirredlem2  31644  chirredlem3  31645  chirredlem4  31646  chirredi  31647  atcvat3i  31649  atcvat4i  31650  atdmd  31651  atmd  31652  atmd2  31653  atabsi  31654  mdsymlem2  31657  mdsymlem3  31658  mdsymlem5  31660  mdsymlem8  31663  atdmd2  31667  sumdmdi  31673  dmdbr4ati  31674  dmdbr5ati  31675  dmdbr6ati  31676