wex - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > wex		Unicode version

Syntax Definition wex 1480

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

**Hypotheses**
Ref	Expression
wph
vx

**Assertion**
Ref	Expression
wex

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

Colors of variables: wff set class