Theorem isprm

Description: The predicate "is a prime number". A prime number is a positive integer with exactly two positive divisors. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	isprm	⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑝 = 𝑃 → ( 𝑛 ∥ 𝑝 ↔ 𝑛 ∥ 𝑃 ) )
2	1	rabbidv	⊢ ( 𝑝 = 𝑃 → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } = { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } )
3	2	breq1d	⊢ ( 𝑝 = 𝑃 → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ) )
4		df-prm	⊢ ℙ = { 𝑝 ∈ ℕ ∣ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝 } ≈ 2o }
5	3 4	elrab2	⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ) )