Theorem atelch 32376

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

Syntax hints:   → wi 4   ∈ wcel 2108   C_ℋ cch 30961  HAtomscat 30997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-at 32370

This theorem is referenced by:  atsseq  32379  atcveq0  32380  chcv1  32387  chcv2  32388  hatomistici  32394  chrelati  32396  chrelat2i  32397  cvati  32398  cvexchlem  32400  cvp  32407  atnemeq0  32409  atcv0eq  32411  atcv1  32412  atexch  32413  atomli  32414  atoml2i  32415  atordi  32416  atcvatlem  32417  atcvati  32418  atcvat2i  32419  chirredlem1  32422  chirredlem2  32423  chirredlem3  32424  chirredlem4  32425  chirredi  32426  atcvat3i  32428  atcvat4i  32429  atdmd  32430  atmd  32431  atmd2  32432  atabsi  32433  mdsymlem2  32436  mdsymlem3  32437  mdsymlem5  32439  mdsymlem8  32442  atdmd2  32446  sumdmdi  32452  dmdbr4ati  32453  dmdbr5ati  32454  dmdbr6ati  32455