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 e. Prime <-> ( P e. NN /\ { n e. NN | n || P } ~~ 2o ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( p = P -> ( n || p <-> n || P ) )
2	1	rabbidv	|- ( p = P -> { n e. NN | n || p } = { n e. NN | n || P } )
3	2	breq1d	|- ( p = P -> ( { n e. NN | n || p } ~~ 2o <-> { n e. NN | n || P } ~~ 2o ) )
4		df-prm	|- Prime = { p e. NN | { n e. NN | n || p } ~~ 2o }
5	3 4	elrab2	|- ( P e. Prime <-> ( P e. NN /\ { n e. NN | n || P } ~~ 2o ) )