Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-ral Structured version   Visualization version   GIF version

Syntax Definition wl-ral 34906
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 34911 for more information.

Colors of variables: wff setvar class
  Copyright terms: Public domain W3C validator