Theorem atelch 32326

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

Syntax hints:   → wi 4   ∈ wcel 2113   C_ℋ cch 30911  HAtomscat 30947

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-ss 3915  df-at 32320

This theorem is referenced by:  atsseq  32329  atcveq0  32330  chcv1  32337  chcv2  32338  hatomistici  32344  chrelati  32346  chrelat2i  32347  cvati  32348  cvexchlem  32350  cvp  32357  atnemeq0  32359  atcv0eq  32361  atcv1  32362  atexch  32363  atomli  32364  atoml2i  32365  atordi  32366  atcvatlem  32367  atcvati  32368  atcvat2i  32369  chirredlem1  32372  chirredlem2  32373  chirredlem3  32374  chirredlem4  32375  chirredi  32376  atcvat3i  32378  atcvat4i  32379  atdmd  32380  atmd  32381  atmd2  32382  atabsi  32383  mdsymlem2  32386  mdsymlem3  32387  mdsymlem5  32389  mdsymlem8  32392  atdmd2  32396  sumdmdi  32402  dmdbr4ati  32403  dmdbr5ati  32404  dmdbr6ati  32405