This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ [\neg_{𝑔} U] = U ⊼_{𝑔} U$

Detailed syntax breakdown

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