\begin{definition}[Definition:Restricted Existential Quantifier]
Let $A$ be a class in ZF.
The '''restricted existential quantifier''' is denoted $\exists x \in A$ and is defined as the following definitional abbreviation:
:$\exists x \in A: \map P x \quad \text{for} \quad \exists x: \paren {x \in A \land \map P x}$
where $\map P x$ is any well-formed formula of the language of set theory.
Category:Definitions/Predicate Logic
Category:Definitions/Zermelo-Fraenkel Class Theory
\end{definition}