Definition df-prm

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprime	|- Prime
1		vp	|- p
2		cn	|- NN
3		vn	|- n
4	3	cv	|- n
5		cdvds	|- ||
6	1	cv	|- p
7	4 6 5	wbr	|- n || p
8	7 3 2	crab	|- { n e. NN | n || p }
9		cen	|- ~~
10		c2o	|- 2o
11	8 10 9	wbr	|- { n e. NN | n || p } ~~ 2o
12	11 1 2	crab	|- { p e. NN | { n e. NN | n || p } ~~ 2o }
13	0 12	wceq	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }