Theorem atelch 29203

Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)

Assertion

Ref	Expression
atelch	|- ( A e. HAtoms -> A e. CH )

Proof of Theorem atelch

Step	Hyp	Ref	Expression
1		atssch 29202	. 2 |- HAtoms C_ CH
2	1	sseli 3599	1 |- ( A e. HAtoms -> A e. CH )

Syntax hints:   -> wi 4   e. wcel 1990   CHcch 27786  HAtomscat 27822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-at 29197

This theorem is referenced by:  atsseq  29206  atcveq0  29207  chcv1  29214  chcv2  29215  hatomistici  29221  chrelati  29223  chrelat2i  29224  cvati  29225  cvexchlem  29227  cvp  29234  atnemeq0  29236  atcv0eq  29238  atcv1  29239  atexch  29240  atomli  29241  atoml2i  29242  atordi  29243  atcvatlem  29244  atcvati  29245  atcvat2i  29246  chirredlem1  29249  chirredlem2  29250  chirredlem3  29251  chirredlem4  29252  chirredi  29253  atcvat3i  29255  atcvat4i  29256  atdmd  29257  atmd  29258  atmd2  29259  atabsi  29260  mdsymlem2  29263  mdsymlem3  29264  mdsymlem5  29266  mdsymlem8  29269  atdmd2  29273  sumdmdi  29279  dmdbr4ati  29280  dmdbr5ati  29281  dmdbr6ati  29282