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

Definition df-goel 23938
Description: Define the Godel-set of membership. Here the arguments  x  =  <. N ,  P >. correspond to vN and vP , so  ( (/)  e.g 
1o ) actually means v0  e. v1 , not  0  e.  1. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-goel  |-  e.g  =  ( x  e.  ( om  X.  om )  |->  <. (/)
,  x >. )

Detailed syntax breakdown of Definition df-goel
StepHypRef Expression
1 cgoe 23931 . 2  class  e.g
2 vx . . 3  set  x
3 com 4672 . . . 4  class  om
43, 3cxp 4703 . . 3  class  ( om 
X.  om )
5 c0 3468 . . . 4  class  (/)
62cv 1631 . . . 4  class  x
75, 6cop 3656 . . 3  class  <. (/) ,  x >.
82, 4, 7cmpt 4093 . 2  class  ( x  e.  ( om  X.  om )  |->  <. (/) ,  x >. )
91, 8wceq 1632 1  wff  e.g  =  ( x  e.  ( om  X.  om )  |->  <. (/)
,  x >. )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator