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

Syntax Definition wl-rex 34363
Description: Redefine the restricted existential 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.
Ref Expression
wph wff 𝜑
vx setvar 𝑥
cA class 𝐴
Ref Expression
wl-rex wff ∃(𝑥 : 𝐴)𝜑

See definition df-wl-rex 34377 for more information.

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