Syntax Definition wmo 1008

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

Hypotheses

Ref	Expression
wph	wff ph
vx	set x

Assertion

Ref	Expression
wmo	wff E*xph

See definition df-mo 1010 for more information.

metamath.org