Theorem atelch 32325

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

Syntax hints:   → wi 4   ∈ wcel 2108   C_ℋ cch 30910  HAtomscat 30946

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943  df-at 32319

This theorem is referenced by:  atsseq  32328  atcveq0  32329  chcv1  32336  chcv2  32337  hatomistici  32343  chrelati  32345  chrelat2i  32346  cvati  32347  cvexchlem  32349  cvp  32356  atnemeq0  32358  atcv0eq  32360  atcv1  32361  atexch  32362  atomli  32363  atoml2i  32364  atordi  32365  atcvatlem  32366  atcvati  32367  atcvat2i  32368  chirredlem1  32371  chirredlem2  32372  chirredlem3  32373  chirredlem4  32374  chirredi  32375  atcvat3i  32377  atcvat4i  32378  atdmd  32379  atmd  32380  atmd2  32381  atabsi  32382  mdsymlem2  32385  mdsymlem3  32386  mdsymlem5  32388  mdsymlem8  32391  atdmd2  32395  sumdmdi  32401  dmdbr4ati  32402  dmdbr5ati  32403  dmdbr6ati  32404