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 E* x ph