Description: Redefine the restricted universal quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from A. x e. A ph with a similiar semantics, but using x as a formal parameter rather than assuming true elementhood.
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-ral |