|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > cwunm | Structured version Visualization version GIF version | ||
| Description: Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset. | 
| Ref | Expression | 
|---|---|
| cwunm | class wUniCl | 
| Colors of variables: wff setvar class | 
| Copyright terms: Public domain | W3C validator |