Definition df-inn 8879

Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 8880 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

Step	Hyp	Ref	Expression
1		cn 8878	. 2 class NN
2		c1 7775	. . . . . 6 class 1
3		vx	. . . . . . 7 setvar x
4	3	cv 1347	. . . . . 6 class x
5	2, 4	wcel 2141	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1347	. . . . . . . 8 class y
8		caddc 7777	. . . . . . . 8 class +
9	7, 2, 8	co 5853	. . . . . . 7 class ( y + 1 )
10	9, 4	wcel 2141	. . . . . 6 wff ( y + 1 ) e. x
11	10, 6, 4	wral 2448	. . . . 5 wff A. y e. x ( y + 1 ) e. x
12	5, 11	wa 103	. . . 4 wff ( 1 e. x /\ A. y e. x ( y + 1 ) e. x )
13	12, 3	cab 2156	. . 3 class { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
14	13	cint 3831	. 2 class |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
15	1, 14	wceq 1348	1 wff NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }

This definition is referenced by:  dfnn2  8880