Definition df-gonot 31335

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

Step	Hyp	Ref	Expression
1		cU	. . 3 class U
2	1	cgon 31328	. 2 class -.g U
3		cgna 31316	. . 3 class |g
4	1, 1, 3	co 6650	. 2 class ( U |g U )
5	2, 4	wceq 1483	1 wff -.g U = ( U |g U )

This definition is referenced by: (None)