Metamath Proof Explorer

Theorem prmssuz2

Description: The primes are integers greater than 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion prmssuz2 
|- Prime C_ ( ZZ>= ` 2 )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( a e. Prime -> a e. ( ZZ>= ` 2 ) )
2 1 ssriv 
 |-  Prime C_ ( ZZ>= ` 2 )