Definition df-inn 9008

Description: Definition of the set of positive integers. For naming consistency with the Metamath Proof Explorer usages should refer to dfnn2 9009 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 9007	. 2 class NN
2		c1 7897	. . . . . 6 class 1
3		vx	. . . . . . 7 setvar x
4	3	cv 1363	. . . . . 6 class x
5	2, 4	wcel 2167	. . . . 5 wff 1 e. x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1363	. . . . . . . 8 class y
8		caddc 7899	. . . . . . . 8 class +
9	7, 2, 8	co 5925	. . . . . . 7 class ( y + 1 )
10	9, 4	wcel 2167	. . . . . 6 wff ( y + 1 ) e. x
11	10, 6, 4	wral 2475	. . . . 5 wff A. y e. x ( y + 1 ) e. x
12	5, 11	wa 104	. . . 4 wff ( 1 e. x /\ A. y e. x ( y + 1 ) e. x )
13	12, 3	cab 2182	. . 3 class { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
14	13	cint 3875	. 2 class |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
15	1, 14	wceq 1364	1 wff NN = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }

This definition is referenced by:  dfnn2  9009