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

Definition df-inn 7696
Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 7697 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  |^|
{  |  1  +  1  }
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-inn
StepHypRef Expression
1 cn 7695 . 2  NN
2 c1 6712 . . . . . 6  1
3 vx . . . . . . 7  setvar
43cv 1241 . . . . . 6
52, 4wcel 1390 . . . . 5  1
6 vy . . . . . . . . 9  setvar
76cv 1241 . . . . . . . 8
8 caddc 6714 . . . . . . . 8  +
97, 2, 8co 5455 . . . . . . 7  +  1
109, 4wcel 1390 . . . . . 6  +  1
1110, 6, 4wral 2300 . . . . 5  +  1
125, 11wa 97 . . . 4 
1  +  1
1312, 3cab 2023 . . 3  {  |  1  +  1  }
1413cint 3606 . 2  |^| {  |  1  +  1  }
151, 14wceq 1242 1  NN  |^|
{  |  1  +  1  }
Colors of variables: wff set class
This definition is referenced by:  dfnn2  7697
  Copyright terms: Public domain W3C validator