Metamath Proof Explorer


Syntax definition w2reu

Description: Syntax for double restricted existential uniqueness quantification.

Ref Expression
Assertion w2reu wff ∃! 𝑥𝐴 , 𝑦𝐵 𝜑