> I want something similar to "obtain" but in definitions (outside of proofs).
If you had uniqueness you could use the "THE" keyword. Something like:
"Q \<equiv> THE Y. P(Y)"
I used it a couple of times, although I prefer different ways of
getting the only set satisfying a predicate.
Since you don't have uniqueness you may check the similar SOME
"Q \<equiv> SOME Y. P(Y)"
It might be what you want but I have never used it so I am not sure.