Syntax Definition wl-rmo 34837

Description: Redefine the restricted "at most one" 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-rmo	wff ∃*(𝑥 : 𝐴)𝜑

See definition df-wl-rmo 34856 for more information.