| Entry | Value |
|---|---|
| Name | EXISTS_UNIQUE_DEF |
| Conclusion | (?!) = (\p. (?) p /\ (!x y. p x /\ p y ==> x = y)) |
| Constructive Proof | Yes |
| Axiom | N|A |
| Classical Lemmas | N|A |
| Constructive Lemmas | N|A |
| Contained Package | bool-def |
| Comment | Standard HOL library retrieved from OpenTheory |