Theorem atelch 32637

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

Syntax hints:   → wi 4   ∈ wcel 2149   C_ℋ cch 31222  HAtomscat 31258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930  df-at 32631

This theorem is referenced by:  atsseq  32640  atcveq0  32641  chcv1  32648  chcv2  32649  hatomistici  32655  chrelati  32657  chrelat2i  32658  cvati  32659  cvexchlem  32661  cvp  32668  atnemeq0  32670  atcv0eq  32672  atcv1  32673  atexch  32674  atomli  32675  atoml2i  32676  atordi  32677  atcvatlem  32678  atcvati  32679  atcvat2i  32680  chirredlem1  32683  chirredlem2  32684  chirredlem3  32685  chirredlem4  32686  chirredi  32687  atcvat3i  32689  atcvat4i  32690  atdmd  32691  atmd  32692  atmd2  32693  atabsi  32694  mdsymlem2  32697  mdsymlem3  32698  mdsymlem5  32700  mdsymlem8  32703  atdmd2  32707  sumdmdi  32713  dmdbr4ati  32714  dmdbr5ati  32715  dmdbr6ati  32716