Description: Syntax for double restricted existential uniqueness quantification.
wff E! x e. A , y e. B ph