Syntax Definition wex 1480

Description: Extend wff definition to include the existential quantifier ("there exists").

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥

Assertion

Ref	Expression
wex	wff ∃𝑥𝜑

This syntax is primitive. The first axiom using it is ax-ie1 1481.