Theorem chsh 9096

Description: A closed subspace is a subspace.

Assertion

Ref	Expression
chsh	|- (H e. CH -> H e. SH)

Proof of Theorem chsh

Step	Hyp	Ref	Expression
1		chsssh 9094	. 2 |- CH (_ SH
2	1	sseli 2065	1 |- (H e. CH -> H e. SH)

Syntax hints:   -> wi 3   e. wcel 958  SHcsh 8797  CHcch 8798

This theorem is referenced by:  chshi 9097  ch0 9098  chss 9099  chocclt 9184  chjvalt 9322  chjclt 9329  ch0let 9365  chle0t 9367  chslejt 9421  chjcomt 9429  chub1t 9430  chlubt 9432  chlej1t 9433  chlej2t 9434  spansnsht 9484  fh1t 9561  fh2t 9562  chsot 9589  pjorth 9614  pjoi0t 9662  hstoct 10149  hstnmoct 10150  ch1dle 10279  atoml 10309  irredlem3 10319  sumdmdi 10342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-ch 9092

Copyright terms: Public domain