| New Foundations Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > NFE Home > Th. List > wreu | Unicode version | ||
| Description: Extend wff notation to include restricted existential uniqueness. | 
| Ref | Expression | 
|---|---|
| wph | 
 | 
| vx | 
 | 
| cA | 
 | 
| Ref | Expression | 
|---|---|
| wreu | 
 | 
| Colors of variables: wff setvar class | 
| Copyright terms: Public domain | W3C validator |