Syntax Definition weu 1007

Description: Extend wff definition to include existential uniqueness ("there exists a unique x such that φ").

Hypotheses

Ref	Expression
wph	wff φ
vx	set x

Assertion

Ref	Expression
weu	wff ∃!xφ

See definition df-eu 1009 for more information.

metamath.org