Syntax Definition wralseu 50598

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

Hypotheses

Ref	Expression
wph	wff 𝜑
wps	wff 𝜓
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
wralseu	wff ∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓)

See definition df-ralseu 50600 for more information.