Database
ELEMENTARY NUMBER THEORY
Elementary prime number theory
Elementary properties
prmex
Next ⟩
0nprm
Metamath Proof Explorer
Ascii
Structured
Theorem
prmex
Description:
The set of prime numbers exists.
(Contributed by
AV
, 22-Jul-2020)
Ref
Expression
Assertion
prmex
⊢
ℙ ∈ V
Proof
Step
Hyp
Ref
Expression
1
nnex
⊢
ℕ ∈ V
2
prmssnn
⊢
ℙ ⊆ ℕ
3
1
2
ssexi
⊢
ℙ ∈ V