Theorem prmssuz2

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

	Ref	Expression
Assertion	prmssuz2	⊢ ℙ ⊆ ( ℤ≥ ‘ 2 )

Proof

Step	Hyp	Ref	Expression
1		prmuz2	⊢ ( 𝑎 ∈ ℙ → 𝑎 ∈ ( ℤ≥ ‘ 2 ) )
2	1	ssriv	⊢ ℙ ⊆ ( ℤ≥ ‘ 2 )