wff-exists - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > wff-exists

Syntax Definition wff-exists 595

Description: Extend WFF definition to include the existential quantifier '∃'.

**Hypotheses**
Ref	Expression
wff-ph	wff 𝜑
objvar-x	objvar 𝑥

**Assertion**
Ref	Expression
wff-exists	wff ∃𝑥𝜑

See definition df-exists-D5.1 596 for more information.

Colors of variables: wff objvar term class