Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gonot Unicode version

Definition df-gonot 23951
Description: Define the Godel-set of negation. Here the argument  U is also a Godel-set corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gonot  |-  -.g U  =  ( U  | g  U )

Detailed syntax breakdown of Definition df-gonot
StepHypRef Expression
1 cU . . 3  class  U
21cgon 23944 . 2  class  -.g U
3 cgna 23932 . . 3  class  | g
41, 1, 3co 5874 . 2  class  ( U 
| g  U )
52, 4wceq 1632 1  wff  -.g U  =  ( U  | g  U )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator