y:T. P(y) 
y = x) }T:Type, P:(T
Prop). {!x:T | P(x)} 
Type| Who Cites unique set? | |
| unique_set | Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y) y = x) } |
| Thm* T:Type, P:(TProp). {!x:T | P(x)} Type |
| Syntax: | {!x:T | P(x)} | has structure: | unique_set(T; x.P(x)) |
About:
 |  |  |  |  |
 |  |  |  |  |