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

Definition df-goex 23942
Description: Define the Godel-set of existential quantification. Here 
N  e.  om corresponds to vN , and  U represents another formula, and this expression is  [ E. x ph ]  =  E.g N U where 
x is the  N-th variable,  U  =  [ ph ] is the code for  ph. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-goex  |-  E.g N U  =  -.g A.g N -.g U

Detailed syntax breakdown of Definition df-goex
StepHypRef Expression
1 cU . . 3  class  U
2 cN . . 3  class  N
31, 2cgox 23935 . 2  class  E.g N U
41cgon 23929 . . . 4  class  -.g U
54, 2cgol 23918 . . 3  class  A.g N -.g U
65cgon 23929 . 2  class  -.g A.g N -.g U
73, 6wceq 1623 1  wff  E.g N U  =  -.g A.g N -.g U
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator