Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gona Unicode version

Definition df-gona 23924
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
StepHypRef Expression
1 cgna 23917 . 2  class  | g
2 vx . . 3  set  x
3 cvv 2788 . . . 4  class  _V
43, 3cxp 4687 . . 3  class  ( _V 
X.  _V )
5 c1o 6472 . . . 4  class  1o
62cv 1622 . . . 4  class  x
75, 6cop 3643 . . 3  class  <. 1o ,  x >.
82, 4, 7cmpt 4077 . 2  class  ( x  e.  ( _V  X.  _V )  |->  <. 1o ,  x >. )
91, 8wceq 1623 1  wff  | g  =  ( x  e.  ( _V  X.  _V )  |->  <. 1o ,  x >. )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator