Theorem atelch 32431

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

Syntax hints:   → wi 4   ∈ wcel 2114   C_ℋ cch 31016  HAtomscat 31052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-at 32425

This theorem is referenced by:  atsseq  32434  atcveq0  32435  chcv1  32442  chcv2  32443  hatomistici  32449  chrelati  32451  chrelat2i  32452  cvati  32453  cvexchlem  32455  cvp  32462  atnemeq0  32464  atcv0eq  32466  atcv1  32467  atexch  32468  atomli  32469  atoml2i  32470  atordi  32471  atcvatlem  32472  atcvati  32473  atcvat2i  32474  chirredlem1  32477  chirredlem2  32478  chirredlem3  32479  chirredlem4  32480  chirredi  32481  atcvat3i  32483  atcvat4i  32484  atdmd  32485  atmd  32486  atmd2  32487  atabsi  32488  mdsymlem2  32491  mdsymlem3  32492  mdsymlem5  32494  mdsymlem8  32497  atdmd2  32501  sumdmdi  32507  dmdbr4ati  32508  dmdbr5ati  32509  dmdbr6ati  32510