weu - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition weu 1372

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 1374 for more information.

Colors of variables: wff set class