Theorem atelch 32280

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

Syntax hints:   → wi 4   ∈ wcel 2109   C_ℋ cch 30865  HAtomscat 30901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-at 32274

This theorem is referenced by:  atsseq  32283  atcveq0  32284  chcv1  32291  chcv2  32292  hatomistici  32298  chrelati  32300  chrelat2i  32301  cvati  32302  cvexchlem  32304  cvp  32311  atnemeq0  32313  atcv0eq  32315  atcv1  32316  atexch  32317  atomli  32318  atoml2i  32319  atordi  32320  atcvatlem  32321  atcvati  32322  atcvat2i  32323  chirredlem1  32326  chirredlem2  32327  chirredlem3  32328  chirredlem4  32329  chirredi  32330  atcvat3i  32332  atcvat4i  32333  atdmd  32334  atmd  32335  atmd2  32336  atabsi  32337  mdsymlem2  32340  mdsymlem3  32341  mdsymlem5  32343  mdsymlem8  32346  atdmd2  32350  sumdmdi  32356  dmdbr4ati  32357  dmdbr5ati  32358  dmdbr6ati  32359