Theorem atelch 32430

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

Syntax hints:   → wi 4   ∈ wcel 2114   C_ℋ cch 31015  HAtomscat 31051

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 3391  df-ss 3907  df-at 32424

This theorem is referenced by:  atsseq  32433  atcveq0  32434  chcv1  32441  chcv2  32442  hatomistici  32448  chrelati  32450  chrelat2i  32451  cvati  32452  cvexchlem  32454  cvp  32461  atnemeq0  32463  atcv0eq  32465  atcv1  32466  atexch  32467  atomli  32468  atoml2i  32469  atordi  32470  atcvatlem  32471  atcvati  32472  atcvat2i  32473  chirredlem1  32476  chirredlem2  32477  chirredlem3  32478  chirredlem4  32479  chirredi  32480  atcvat3i  32482  atcvat4i  32483  atdmd  32484  atmd  32485  atmd2  32486  atabsi  32487  mdsymlem2  32490  mdsymlem3  32491  mdsymlem5  32493  mdsymlem8  32496  atdmd2  32500  sumdmdi  32506  dmdbr4ati  32507  dmdbr5ati  32508  dmdbr6ati  32509