Syntax Definition walsc 13953

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

Hypotheses

Ref	Expression
wph	wff ph
vx	setvar x
cA	class A

Assertion

Ref	Expression
walsc	wff A.! x e. A ph

See definition df-alsc 13955 for more information.