Theorem atelch 30115

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

Syntax hints:   → wi 4   ∈ wcel 2110   C_ℋ cch 28700  HAtomscat 28736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951  df-at 30109

This theorem is referenced by:  atsseq  30118  atcveq0  30119  chcv1  30126  chcv2  30127  hatomistici  30133  chrelati  30135  chrelat2i  30136  cvati  30137  cvexchlem  30139  cvp  30146  atnemeq0  30148  atcv0eq  30150  atcv1  30151  atexch  30152  atomli  30153  atoml2i  30154  atordi  30155  atcvatlem  30156  atcvati  30157  atcvat2i  30158  chirredlem1  30161  chirredlem2  30162  chirredlem3  30163  chirredlem4  30164  chirredi  30165  atcvat3i  30167  atcvat4i  30168  atdmd  30169  atmd  30170  atmd2  30171  atabsi  30172  mdsymlem2  30175  mdsymlem3  30176  mdsymlem5  30178  mdsymlem8  30181  atdmd2  30185  sumdmdi  30191  dmdbr4ati  30192  dmdbr5ati  30193  dmdbr6ati  30194