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

Definition df-goel 23923
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 23916 . 2  class  e.g
2 vx . . 3  set  x
3 com 4656 . . . 4  class  om
43, 3cxp 4687 . . 3  class  ( om 
X.  om )
5 c0 3455 . . . 4  class  (/)
62cv 1622 . . . 4  class  x
75, 6cop 3643 . . 3  class  <. (/) ,  x >.
82, 4, 7cmpt 4077 . 2  class  ( x  e.  ( om  X.  om )  |->  <. (/) ,  x >. )
91, 8wceq 1623 1  wff  e.g  =  ( x  e.  ( om  X.  om )  |->  <. (/)
,  x >. )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator