Theorem atelch 32928

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   C_ℋ cch 31513  HAtomscat 31549

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-at 32922

This theorem is used by:  atsseq  32931  atcveq0  32932  chcv1  32939  chcv2  32940  hatomistici  32946  chrelati  32948  chrelat2i  32949  cvati  32950  cvexchlem  32952  cvp  32959  atnemeq0  32961  atcv0eq  32963  atcv1  32964  atexch  32965  atomli  32966  atoml2i  32967  atordi  32968  atcvatlem  32969  atcvati  32970  atcvat2i  32971  chirredlem1  32974  chirredlem2  32975  chirredlem3  32976  chirredlem4  32977  chirredi  32978  atcvat3i  32980  atcvat4i  32981  atdmd  32982  atmd  32983  atmd2  32984  atabsi  32985  mdsymlem2  32988  mdsymlem3  32989  mdsymlem5  32991  mdsymlem8  32994  atdmd2  32998  sumdmdi  33004  dmdbr4ati  33005  dmdbr5ati  33006  dmdbr6ati  33007