Syntax Definition walseu 50597

Description: Extend wff definition to include "all some one" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and exactly one 𝑥 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)

Hypotheses

Ref	Expression
wph	wff 𝜑
wps	wff 𝜓
vx	setvar 𝑥

Assertion

Ref	Expression
walseu	wff ∀∃!𝑥(𝜑 → 𝜓)

See definition df-alseu 50599 for more information.