Theorem atelch 32331

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

Syntax hints:   → wi 4   ∈ wcel 2111   C_ℋ cch 30916  HAtomscat 30952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-at 32325

This theorem is referenced by:  atsseq  32334  atcveq0  32335  chcv1  32342  chcv2  32343  hatomistici  32349  chrelati  32351  chrelat2i  32352  cvati  32353  cvexchlem  32355  cvp  32362  atnemeq0  32364  atcv0eq  32366  atcv1  32367  atexch  32368  atomli  32369  atoml2i  32370  atordi  32371  atcvatlem  32372  atcvati  32373  atcvat2i  32374  chirredlem1  32377  chirredlem2  32378  chirredlem3  32379  chirredlem4  32380  chirredi  32381  atcvat3i  32383  atcvat4i  32384  atdmd  32385  atmd  32386  atmd2  32387  atabsi  32388  mdsymlem2  32391  mdsymlem3  32392  mdsymlem5  32394  mdsymlem8  32397  atdmd2  32401  sumdmdi  32407  dmdbr4ati  32408  dmdbr5ati  32409  dmdbr6ati  32410