Metamath Proof Explorer


Syntax definition wmoo

Description: Syntax for BJ's version of the uniqueness quantifier.

Ref Expression
Assertion wmoo
wff E** x ph