MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lssel Structured version   Unicode version

Theorem lssel 16006
Description: A subspace member is a vector. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 8-Jan-2015.)
Hypotheses
Ref Expression
lssss.v  |-  V  =  ( Base `  W
)
lssss.s  |-  S  =  ( LSubSp `  W )
Assertion
Ref Expression
lssel  |-  ( ( U  e.  S  /\  X  e.  U )  ->  X  e.  V )

Proof of Theorem lssel
StepHypRef Expression
1 lssss.v . . 3  |-  V  =  ( Base `  W
)
2 lssss.s . . 3  |-  S  =  ( LSubSp `  W )
31, 2lssss 16005 . 2  |-  ( U  e.  S  ->  U  C_  V )
43sselda 3340 1  |-  ( ( U  e.  S  /\  X  e.  U )  ->  X  e.  V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   ` cfv 5446   Basecbs 13461   LSubSpclss 16000
This theorem is referenced by:  lssvsubcl  16012  lssvancl1  16013  lssvancl2  16014  lss0cl  16015  lssvacl  16022  lssvscl  16023  lssvnegcl  16024  lspsnel6  16062  lspsnel5a  16064  lssats2  16068  lsmcl  16147  lsmelval2  16149  lsmcv  16205  ocvin  16893  lsatel  29740  lsmsat  29743  lssatomic  29746  lssats  29747  lsat0cv  29768  lshpkrlem1  29845  lshpkrlem5  29849  lshpkr  29852  dihjat1lem  32163  dochsatshpb  32187  lcfrvalsnN  32276  lcfrlem4  32280  lcfrlem6  32282  lcfrlem16  32293  lcfrlem29  32306  lcfrlem35  32312  mapdval4N  32367  mapdpglem2a  32409  mapdpglem23  32429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fv 5454  df-ov 6076  df-lss 16001
  Copyright terms: Public domain W3C validator