Syntax Definition wral 2448

Description: Extend wff notation to include restricted universal quantification.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
wral	wff ∀𝑥 ∈ 𝐴 𝜑

See definition df-ral 2453 for more information.