Theorem atelch 32605

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

Syntax hints:   → wi 4   ∈ wcel 2145   C_ℋ cch 31190  HAtomscat 31226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-at 32599

This theorem is referenced by:  atsseq  32608  atcveq0  32609  chcv1  32616  chcv2  32617  hatomistici  32623  chrelati  32625  chrelat2i  32626  cvati  32627  cvexchlem  32629  cvp  32636  atnemeq0  32638  atcv0eq  32640  atcv1  32641  atexch  32642  atomli  32643  atoml2i  32644  atordi  32645  atcvatlem  32646  atcvati  32647  atcvat2i  32648  chirredlem1  32651  chirredlem2  32652  chirredlem3  32653  chirredlem4  32654  chirredi  32655  atcvat3i  32657  atcvat4i  32658  atdmd  32659  atmd  32660  atmd2  32661  atabsi  32662  mdsymlem2  32665  mdsymlem3  32666  mdsymlem5  32668  mdsymlem8  32671  atdmd2  32675  sumdmdi  32681  dmdbr4ati  32682  dmdbr5ati  32683  dmdbr6ati  32684