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

Syntax Definition wex 1354
Description: Extend wff definition to include the existential quantifier ("there exists").
Hypotheses
Ref Expression
wph
vx  setvar
Assertion
Ref Expression
wex

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

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator