Syntax Definition wl-rex 35277

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.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
wl-rex	wff ∃(𝑥 : 𝐴)𝜑

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