Syntax Definition walsc 13953

Description: Extend wff definition to include "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.)

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
cA	class 𝐴

Assertion

Ref	Expression
walsc	wff ∀!𝑥 ∈ 𝐴𝜑

See definition df-alsc 13955 for more information.