Theorem atelch 32273

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

Syntax hints:   → wi 4   ∈ wcel 2109   C_ℋ cch 30858  HAtomscat 30894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-at 32267

This theorem is referenced by:  atsseq  32276  atcveq0  32277  chcv1  32284  chcv2  32285  hatomistici  32291  chrelati  32293  chrelat2i  32294  cvati  32295  cvexchlem  32297  cvp  32304  atnemeq0  32306  atcv0eq  32308  atcv1  32309  atexch  32310  atomli  32311  atoml2i  32312  atordi  32313  atcvatlem  32314  atcvati  32315  atcvat2i  32316  chirredlem1  32319  chirredlem2  32320  chirredlem3  32321  chirredlem4  32322  chirredi  32323  atcvat3i  32325  atcvat4i  32326  atdmd  32327  atmd  32328  atmd2  32329  atabsi  32330  mdsymlem2  32333  mdsymlem3  32334  mdsymlem5  32336  mdsymlem8  32339  atdmd2  32343  sumdmdi  32349  dmdbr4ati  32350  dmdbr5ati  32351  dmdbr6ati  32352