Definition df-prm 15224

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

Assertion

Ref	Expression
df-prm	⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2𝑜}

Distinct variable group:   𝑛,𝑝

Detailed syntax breakdown of Definition df-prm

Step	Hyp	Ref	Expression
1		cprime 15223	. 2 class ℙ
2		vn	. . . . . . 7 setvar 𝑛
3	2	cv 1474	. . . . . 6 class 𝑛
4		vp	. . . . . . 7 setvar 𝑝
5	4	cv 1474	. . . . . 6 class 𝑝
6		cdvds 14821	. . . . . 6 class ∥
7	3, 5, 6	wbr 4583	. . . . 5 wff 𝑛 ∥ 𝑝
8		cn 10897	. . . . 5 class ℕ
9	7, 2, 8	crab 2900	. . . 4 class {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝}
10		c2o 7441	. . . 4 class 2𝑜
11		cen 7838	. . . 4 class ≈
12	9, 10, 11	wbr 4583	. . 3 wff {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2𝑜
13	12, 4, 8	crab 2900	. 2 class {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2𝑜}
14	1, 13	wceq 1475	1 wff ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2𝑜}

This definition is referenced by:  isprm  15225