Theorem atelch 32951

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   C_ℋ cch 31536  HAtomscat 31572

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-at 32945

This theorem is used by:  atsseq  32954  atcveq0  32955  chcv1  32962  chcv2  32963  hatomistici  32969  chrelati  32971  chrelat2i  32972  cvati  32973  cvexchlem  32975  cvp  32982  atnemeq0  32984  atcv0eq  32986  atcv1  32987  atexch  32988  atomli  32989  atoml2i  32990  atordi  32991  atcvatlem  32992  atcvati  32993  atcvat2i  32994  chirredlem1  32997  chirredlem2  32998  chirredlem3  32999  chirredlem4  33000  chirredi  33001  atcvat3i  33003  atcvat4i  33004  atdmd  33005  atmd  33006  atmd2  33007  atabsi  33008  mdsymlem2  33011  mdsymlem3  33012  mdsymlem5  33014  mdsymlem8  33017  atdmd2  33021  sumdmdi  33027  dmdbr4ati  33028  dmdbr5ati  33029  dmdbr6ati  33030