Definition df-prm 12886

Description: Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.)

Assertion

Ref	Expression
df-prm	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }

Distinct variable group:   n, p

Detailed syntax breakdown of Definition df-prm

Step	Hyp	Ref	Expression
1		cprime 12885	. 2 class Prime
2		vn	. . . . . . 7 setvar n
3	2	cv 1401	. . . . . 6 class n
4		vp	. . . . . . 7 setvar p
5	4	cv 1401	. . . . . 6 class p
6		cdvds 12554	. . . . . 6 class ||
7	3, 5, 6	wbr 4130	. . . . 5 wff n || p
8		cn 9304	. . . . 5 class NN
9	7, 2, 8	crab 2532	. . . 4 class { n e. NN | n || p }
10		c2o 6681	. . . 4 class 2o
11		cen 7020	. . . 4 class ~~
12	9, 10, 11	wbr 4130	. . 3 wff { n e. NN | n || p } ~~ 2o
13	12, 4, 8	crab 2532	. 2 class { p e. NN | { n e. NN | n || p } ~~ 2o }
14	1, 13	wceq 1402	1 wff Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }

This definition is used by:  isprm  12887