Theorem atelch 30702

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

Syntax hints:   → wi 4   ∈ wcel 2110   C_ℋ cch 29287  HAtomscat 29323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909  df-at 30696

This theorem is referenced by:  atsseq  30705  atcveq0  30706  chcv1  30713  chcv2  30714  hatomistici  30720  chrelati  30722  chrelat2i  30723  cvati  30724  cvexchlem  30726  cvp  30733  atnemeq0  30735  atcv0eq  30737  atcv1  30738  atexch  30739  atomli  30740  atoml2i  30741  atordi  30742  atcvatlem  30743  atcvati  30744  atcvat2i  30745  chirredlem1  30748  chirredlem2  30749  chirredlem3  30750  chirredlem4  30751  chirredi  30752  atcvat3i  30754  atcvat4i  30755  atdmd  30756  atmd  30757  atmd2  30758  atabsi  30759  mdsymlem2  30762  mdsymlem3  30763  mdsymlem5  30765  mdsymlem8  30768  atdmd2  30772  sumdmdi  30778  dmdbr4ati  30779  dmdbr5ati  30780  dmdbr6ati  30781