Syntax Definition weu 2204

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

Hypotheses

Ref	Expression
wph	wff φ
vx	setvar x

Assertion

Ref	Expression
weu	wff ∃!xφ

See definition df-eu 2208 for more information.