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

Metamath Proof Explorer

Definition df-gona

Description: Define the Godel-set for the Sheffer stroke NAND. Here the arguments x = <. U , V >. are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-gona	$⊢ ⊼_{𝑔} = (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgna	$class ⊼_{𝑔}$
1		vx	$setvar x$
2		cvv	$class V$
3	2 2	cxp	$class (V \times V)$
4		c1o	$class 1_{𝑜}$
5	1	cv	$setvar x$
6	4 5	cop	$class ⟨1_{𝑜}, x⟩$
7	1 3 6	cmpt	$class (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$
8	0 7	wceq	$wff ⊼_{𝑔} = (x \in (V \times V) ⟼ ⟨1_{𝑜}, x⟩)$