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

Definition df-ssp 22221
 Description: Define the class of all subspaces of complex normed vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-ssp CV CV
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ssp
StepHypRef Expression
1 css 22220 . 2
2 vu . . 3
3 cnv 22063 . . 3
4 vw . . . . . . . 8
54cv 1651 . . . . . . 7
6 cpv 22064 . . . . . . 7
75, 6cfv 5454 . . . . . 6
82cv 1651 . . . . . . 7
98, 6cfv 5454 . . . . . 6
107, 9wss 3320 . . . . 5
11 cns 22066 . . . . . . 7
125, 11cfv 5454 . . . . . 6
138, 11cfv 5454 . . . . . 6
1412, 13wss 3320 . . . . 5
15 cnmcv 22069 . . . . . . 7 CV
165, 15cfv 5454 . . . . . 6 CV
178, 15cfv 5454 . . . . . 6 CV
1816, 17wss 3320 . . . . 5 CV CV
1910, 14, 18w3a 936 . . . 4 CV CV
2019, 4, 3crab 2709 . . 3 CV CV
212, 3, 20cmpt 4266 . 2 CV CV
221, 21wceq 1652 1 CV CV
 Colors of variables: wff set class This definition is referenced by:  sspval  22222
 Copyright terms: Public domain W3C validator