Theorem atelch 32833

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   C_ℋ cch 31418  HAtomscat 31454

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-at 32827

This theorem is used by:  atsseq  32836  atcveq0  32837  chcv1  32844  chcv2  32845  hatomistici  32851  chrelati  32853  chrelat2i  32854  cvati  32855  cvexchlem  32857  cvp  32864  atnemeq0  32866  atcv0eq  32868  atcv1  32869  atexch  32870  atomli  32871  atoml2i  32872  atordi  32873  atcvatlem  32874  atcvati  32875  atcvat2i  32876  chirredlem1  32879  chirredlem2  32880  chirredlem3  32881  chirredlem4  32882  chirredi  32883  atcvat3i  32885  atcvat4i  32886  atdmd  32887  atmd  32888  atmd2  32889  atabsi  32890  mdsymlem2  32893  mdsymlem3  32894  mdsymlem5  32896  mdsymlem8  32899  atdmd2  32903  sumdmdi  32909  dmdbr4ati  32910  dmdbr5ati  32911  dmdbr6ati  32912