Definition df-gona 31323

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

Assertion

Ref	Expression
df-gona	|- |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )

Detailed syntax breakdown of Definition df-gona

Step	Hyp	Ref	Expression
1		cgna 31316	. 2 class |g
2		vx	. . 3 setvar x
3		cvv 3200	. . . 4 class _V
4	3, 3	cxp 5112	. . 3 class ( _V X. _V )
5		c1o 7553	. . . 4 class 1o
6	2	cv 1482	. . . 4 class x
7	5, 6	cop 4183	. . 3 class <. 1o , x >.
8	2, 4, 7	cmpt 4729	. 2 class ( x e. ( _V X. _V ) |-> <. 1o , x >. )
9	1, 8	wceq 1483	1 wff |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )

This definition is referenced by: (None)