Theorem atelch 28587

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

Syntax hints:   → wi 4   ∈ wcel 1977   C_ℋ cch 27170  HAtomscat 27206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-in 3547  df-ss 3554  df-at 28581

This theorem is referenced by:  atsseq  28590  atcveq0  28591  chcv1  28598  chcv2  28599  hatomistici  28605  chrelati  28607  chrelat2i  28608  cvati  28609  cvexchlem  28611  cvp  28618  atnemeq0  28620  atcv0eq  28622  atcv1  28623  atexch  28624  atomli  28625  atoml2i  28626  atordi  28627  atcvatlem  28628  atcvati  28629  atcvat2i  28630  chirredlem1  28633  chirredlem2  28634  chirredlem3  28635  chirredlem4  28636  chirredi  28637  atcvat3i  28639  atcvat4i  28640  atdmd  28641  atmd  28642  atmd2  28643  atabsi  28644  mdsymlem2  28647  mdsymlem3  28648  mdsymlem5  28650  mdsymlem8  28653  atdmd2  28657  sumdmdi  28663  dmdbr4ati  28664  dmdbr5ati  28665  dmdbr6ati  28666