Syntax Definition wl-reu 34836

Description: Redefine the restricted existential uniqueness 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-reu	wff ∃!(𝑥 : 𝐴)𝜑

See definition df-wl-reu 34858 for more information.