df-prm

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

		Ref	Expression
	Assertion	df-prm	$⊢ ℙ = \{p \in ℕ \| \{n \in ℕ \| n ∥ p\} \approx 2_{𝑜}\}$

Step	Hyp	Ref	Expression
0		cprime	$class ℙ$
1		vp	$setvar p$
2		cn	$class ℕ$
3		vn	$setvar n$
4	3	cv	$setvar n$
5		cdvds	$class ∥$
6	1	cv	$setvar p$
7	4 6 5	wbr	$wff n ∥ p$
8	7 3 2	crab	$class \{n \in ℕ \| n ∥ p\}$
9		cen	$class \approx$
10		c2o	$class 2_{𝑜}$
11	8 10 9	wbr	$wff \{n \in ℕ \| n ∥ p\} \approx 2_{𝑜}$
12	11 1 2	crab	$class \{p \in ℕ \| \{n \in ℕ \| n ∥ p\} \approx 2_{𝑜}\}$
13	0 12	wceq	$wff ℙ = \{p \in ℕ \| \{n \in ℕ \| n ∥ p\} \approx 2_{𝑜}\}$

Metamath Proof Explorer