Syntax Definition wex 678

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

Hypotheses

Ref	Expression
wph	wff φ
vx	set x

Assertion

Ref	Expression
wex	wff ∃xφ

See definition df-ex 679 for more information.

metamath.org