Metamath Proof Explorer


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