Soundness justification theorem for eu6 when this was the definition of the unique existential quantifier (note that \( y \) and \( z \) need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT for a proof that provides an example of how it can be achieved through the use of dvelim. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)