Definition df-gonot 30589

Description: Define the Godel-set of negation. Here the argument 𝑈 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	⊢ ¬𝑔𝑈 = (𝑈⊼𝑔𝑈)

Detailed syntax breakdown of Definition df-gonot

Step	Hyp	Ref	Expression
1		cU	. . 3 class 𝑈
2	1	cgon 30582	. 2 class ¬𝑔𝑈
3		cgna 30570	. . 3 class ⊼𝑔
4	1, 1, 3	co 6549	. 2 class (𝑈⊼𝑔𝑈)
5	2, 4	wceq 1475	1 wff ¬𝑔𝑈 = (𝑈⊼𝑔𝑈)

This definition is referenced by: (None)