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	$$⊢{⊼}_{𝑔}=\left(x\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨1_{𝑜},x⟩\right)$$

Detailed syntax breakdown

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