[Agda] How to formalize 'there exists a set' phrase?

[Vag Vagoff]

> data ∃ (P : Set → Set) : Set₁ where
> _,_ : (A : Set) → P A → ∃ P

Okay. But it is still unknown how to state "There exist a subset of A that property P holds" (i.e. "there exist a set of primes")

Thanks in advance,
sincerely yours,
Vag.