Definition df-prm

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

	Ref	Expression
Assertion	df-prm	$$⊢\mathbb{P}=\left\{p\in \mathbb{N}|\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprime	$$class\mathbb{P}$$
1		vp	$$setvarp$$
2		cn	$$class\mathbb{N}$$
3		vn	$$setvarn$$
4	3	cv	$$setvarn$$
5		cdvds	$$class\parallel$$
6	1	cv	$$setvarp$$
7	4 6 5	wbr	$$wffn\parallel p$$
8	7 3 2	crab	$$class\left\{n\in \mathbb{N}|n\parallel p\right\}$$
9		cen	$$class\approx$$
10		c2o	$$class{2}_{𝑜}$$
11	8 10 9	wbr	$$wff\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}$$
12	11 1 2	crab	$$class\left\{p\in \mathbb{N}|\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}\right\}$$
13	0 12	wceq	$$wff\mathbb{P}=\left\{p\in \mathbb{N}|\left\{n\in \mathbb{N}|n\parallel p\right\}\approx 2_{𝑜}\right\}$$