Theorem atelch 32733

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   C_ℋ cch 31318  HAtomscat 31354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925  df-at 32727

This theorem is used by:  atsseq  32736  atcveq0  32737  chcv1  32744  chcv2  32745  hatomistici  32751  chrelati  32753  chrelat2i  32754  cvati  32755  cvexchlem  32757  cvp  32764  atnemeq0  32766  atcv0eq  32768  atcv1  32769  atexch  32770  atomli  32771  atoml2i  32772  atordi  32773  atcvatlem  32774  atcvati  32775  atcvat2i  32776  chirredlem1  32779  chirredlem2  32780  chirredlem3  32781  chirredlem4  32782  chirredi  32783  atcvat3i  32785  atcvat4i  32786  atdmd  32787  atmd  32788  atmd2  32789  atabsi  32790  mdsymlem2  32793  mdsymlem3  32794  mdsymlem5  32796  mdsymlem8  32799  atdmd2  32803  sumdmdi  32809  dmdbr4ati  32810  dmdbr5ati  32811  dmdbr6ati  32812