Metamath Proof Explorer


Syntax definition wex

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

Ref Expression
Assertion wex
wff E. x ph