Theorem atelch 32363

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

Syntax hints:   → wi 4   ∈ wcel 2108   C_ℋ cch 30948  HAtomscat 30984

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-at 32357

This theorem is referenced by:  atsseq  32366  atcveq0  32367  chcv1  32374  chcv2  32375  hatomistici  32381  chrelati  32383  chrelat2i  32384  cvati  32385  cvexchlem  32387  cvp  32394  atnemeq0  32396  atcv0eq  32398  atcv1  32399  atexch  32400  atomli  32401  atoml2i  32402  atordi  32403  atcvatlem  32404  atcvati  32405  atcvat2i  32406  chirredlem1  32409  chirredlem2  32410  chirredlem3  32411  chirredlem4  32412  chirredi  32413  atcvat3i  32415  atcvat4i  32416  atdmd  32417  atmd  32418  atmd2  32419  atabsi  32420  mdsymlem2  32423  mdsymlem3  32424  mdsymlem5  32426  mdsymlem8  32429  atdmd2  32433  sumdmdi  32439  dmdbr4ati  32440  dmdbr5ati  32441  dmdbr6ati  32442