ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-inn Unicode version

Definition df-inn 7990
Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 7991 instead. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.) (New usage is discouraged.)
Assertion
Ref Expression
df-inn  |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-inn
StepHypRef Expression
1 cn 7989 . 2  class  NN
2 c1 6947 . . . . . 6  class  1
3 vx . . . . . . 7  setvar  x
43cv 1258 . . . . . 6  class  x
52, 4wcel 1409 . . . . 5  wff  1  e.  x
6 vy . . . . . . . . 9  setvar  y
76cv 1258 . . . . . . . 8  class  y
8 caddc 6949 . . . . . . . 8  class  +
97, 2, 8co 5539 . . . . . . 7  class  ( y  +  1 )
109, 4wcel 1409 . . . . . 6  wff  ( y  +  1 )  e.  x
1110, 6, 4wral 2323 . . . . 5  wff  A. y  e.  x  ( y  +  1 )  e.  x
125, 11wa 101 . . . 4  wff  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x )
1312, 3cab 2042 . . 3  class  { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
1413cint 3642 . 2  class  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
151, 14wceq 1259 1  wff  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
Colors of variables: wff set class
This definition is referenced by:  dfnn2  7991
  Copyright terms: Public domain W3C validator