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