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

Definition df-goal 23925
Description: Define the Godel-set of universal quantification. Here  N  e.  om corresponds to vN , and  U represents another formula, and this expression is  [ A. x ph ]  =  A.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-goal  |-  A.g N U  =  <. 2o ,  <. N ,  U >. >.

Detailed syntax breakdown of Definition df-goal
StepHypRef Expression
1 cU . . 3  class  U
2 cN . . 3  class  N
31, 2cgol 23918 . 2  class  A.g N U
4 c2o 6473 . . 3  class  2o
52, 1cop 3643 . . 3  class  <. N ,  U >.
64, 5cop 3643 . 2  class  <. 2o ,  <. N ,  U >. >.
73, 6wceq 1623 1  wff  A.g N U  =  <. 2o ,  <. N ,  U >. >.
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator