Syntax Definition wl-ral 34833

Description: Redefine the restricted universal quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from ∀𝑥 ∈ 𝐴𝜑 with a similiar semantics, but using 𝑥 as a formal parameter rather than assuming true elementhood.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
wl-ral	wff ∀(𝑥 : 𝐴)𝜑

See definition df-wl-ral 34838 for more information.