Metamath Proof Explorer


Syntax definition wmo

Description: Extend wff definition to include the at-most-one quantifier ("there exists at most one x such that ph ").

Ref Expression
Assertion wmo wff ∃* 𝑥 𝜑