Definition:Restricted Universal Quantifier

Definition

Let $A$ be a class in ZF.

The restricted universal quantifier is denoted $\forall x \in A$ and is defined as the following definitional abbreviation:

$\forall x \in A: \map P x \quad \text{for} \quad \forall x: \paren {x \in A \implies \map P x}$

where $\map P x$ is any well-formed formula of the language of set theory.