Metamath Proof Explorer


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 P P n | n P 2 𝑜

Proof

Step Hyp Ref Expression
1 breq2 p = P n p n P
2 1 rabbidv p = P n | n p = n | n P
3 2 breq1d p = P n | n p 2 𝑜 n | n P 2 𝑜
4 df-prm = p | n | n p 2 𝑜
5 3 4 elrab2 P P n | n P 2 𝑜