Theorem atelch 32415

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

Syntax hints:   → wi 4   ∈ wcel 2114   C_ℋ cch 31000  HAtomscat 31036

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-at 32409

This theorem is referenced by:  atsseq  32418  atcveq0  32419  chcv1  32426  chcv2  32427  hatomistici  32433  chrelati  32435  chrelat2i  32436  cvati  32437  cvexchlem  32439  cvp  32446  atnemeq0  32448  atcv0eq  32450  atcv1  32451  atexch  32452  atomli  32453  atoml2i  32454  atordi  32455  atcvatlem  32456  atcvati  32457  atcvat2i  32458  chirredlem1  32461  chirredlem2  32462  chirredlem3  32463  chirredlem4  32464  chirredi  32465  atcvat3i  32467  atcvat4i  32468  atdmd  32469  atmd  32470  atmd2  32471  atabsi  32472  mdsymlem2  32475  mdsymlem3  32476  mdsymlem5  32478  mdsymlem8  32481  atdmd2  32485  sumdmdi  32491  dmdbr4ati  32492  dmdbr5ati  32493  dmdbr6ati  32494