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

Theorem lssel 19998
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 𝑉 = (Base‘𝑊)
lssss.s 𝑆 = (LSubSp‘𝑊)
Assertion
Ref Expression
lssel ((𝑈𝑆𝑋𝑈) → 𝑋𝑉)

Proof of Theorem lssel
StepHypRef Expression
1 lssss.v . . 3 𝑉 = (Base‘𝑊)
2 lssss.s . . 3 𝑆 = (LSubSp‘𝑊)
31, 2lssss 19997 . 2 (𝑈𝑆𝑈𝑉)
43sselda 3915 1 ((𝑈𝑆𝑋𝑈) → 𝑋𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2111  cfv 6397  Basecbs 16784  LSubSpclss 19992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-iota 6355  df-fun 6399  df-fv 6405  df-ov 7234  df-lss 19993
This theorem is referenced by:  lssvsubcl  20004  lssvancl1  20005  lssvancl2  20006  lss0cl  20007  lssvacl  20015  lssvscl  20016  lssvnegcl  20017  lspsnel6  20055  lspsnel5a  20057  lssats2  20061  lsmcl  20144  lsmelval2  20146  lsmcv  20202  ocvin  20660  lsatel  36782  lsmsat  36785  lssatomic  36788  lssats  36789  lsat0cv  36810  lshpkrlem1  36887  lshpkrlem5  36891  lshpkr  36894  dihjat1lem  39205  dochsatshpb  39229  lcfrvalsnN  39318  lcfrlem4  39322  lcfrlem6  39324  lcfrlem16  39335  lcfrlem29  39348  lcfrlem35  39354  mapdval4N  39409  mapdpglem2a  39451  mapdpglem23  39471
  Copyright terms: Public domain W3C validator