Theorem atelch 30123

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

Syntax hints:   → wi 4   ∈ wcel 2114   C_ℋ cch 28708  HAtomscat 28744

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-in 3945  df-ss 3954  df-at 30117

This theorem is referenced by:  atsseq  30126  atcveq0  30127  chcv1  30134  chcv2  30135  hatomistici  30141  chrelati  30143  chrelat2i  30144  cvati  30145  cvexchlem  30147  cvp  30154  atnemeq0  30156  atcv0eq  30158  atcv1  30159  atexch  30160  atomli  30161  atoml2i  30162  atordi  30163  atcvatlem  30164  atcvati  30165  atcvat2i  30166  chirredlem1  30169  chirredlem2  30170  chirredlem3  30171  chirredlem4  30172  chirredi  30173  atcvat3i  30175  atcvat4i  30176  atdmd  30177  atmd  30178  atmd2  30179  atabsi  30180  mdsymlem2  30183  mdsymlem3  30184  mdsymlem5  30186  mdsymlem8  30189  atdmd2  30193  sumdmdi  30199  dmdbr4ati  30200  dmdbr5ati  30201  dmdbr6ati  30202