Theorem atelch 32274

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

Syntax hints:   → wi 4   ∈ wcel 2099   C_ℋ cch 30859  HAtomscat 30895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-ss 3963  df-at 32268

This theorem is referenced by:  atsseq  32277  atcveq0  32278  chcv1  32285  chcv2  32286  hatomistici  32292  chrelati  32294  chrelat2i  32295  cvati  32296  cvexchlem  32298  cvp  32305  atnemeq0  32307  atcv0eq  32309  atcv1  32310  atexch  32311  atomli  32312  atoml2i  32313  atordi  32314  atcvatlem  32315  atcvati  32316  atcvat2i  32317  chirredlem1  32320  chirredlem2  32321  chirredlem3  32322  chirredlem4  32323  chirredi  32324  atcvat3i  32326  atcvat4i  32327  atdmd  32328  atmd  32329  atmd2  32330  atabsi  32331  mdsymlem2  32334  mdsymlem3  32335  mdsymlem5  32337  mdsymlem8  32340  atdmd2  32344  sumdmdi  32350  dmdbr4ati  32351  dmdbr5ati  32352  dmdbr6ati  32353