Metamath Proof Explorer


Syntax definition wex

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

Ref Expression
Assertion wex wff 𝑥 𝜑