Definition df-gonot

Description: Define the Godel-set of negation. Here the argument U is also a Godel-set corresponding to smaller formulas. Note that this is aclass expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-gonot	$$⊢\left[{\neg }_{𝑔}U\right]=U{⊼}_{𝑔}U$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cU	$$classU$$
1	0	cgon	$$class\left[{\neg }_{𝑔}U\right]$$
2		cgna	$$class{⊼}_{𝑔}$$
3	0 0 2	co	$$class\left(U{⊼}_{𝑔}U\right)$$
4	1 3	wceq	$$wff\left[{\neg }_{𝑔}U\right]=U{⊼}_{𝑔}U$$