Metamath Proof Explorer

Theorem prmex

Description: The set of prime numbers exists. (Contributed by AV, 22-Jul-2020)

Ref Expression
Assertion prmex 
|- Prime e. _V

Proof

Step Hyp Ref Expression
1 nnex 
 |-  NN e. _V
2 prmssnn 
 |-  Prime C_ NN
3 1 2 ssexi 
 |-  Prime e. _V