English
If there exists a unique x with p x, and for every x with p x, whenever q x holds, and whenever any y with p y implies y = x, then b.
Русский
Если существует единственный x с p(x), и для каждого x с p(x) верно, что q(x), и если для любого y с p(y) следует y = x, то выполнится b.
LaTeX
$$$$ (\\\\exists! x, p(x)) \\rightarrow \\left( \\forall x\\\\, p(x) \\rightarrow (\\\\forall y\\\\, p(y) \\\\rightarrow y = x) \\\\rightarrow b \\right) \\rightarrow b. $$$$
Lean4
theorem elim {p : α → Prop} {b : Prop} (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
Exists.elim h₂ (fun w hw ↦ h₁ w (And.left hw) (And.right hw))
