Syntax Definition walsi 13952

Description: Extend wff definition to include "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and there is at least least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.)

Hypotheses

Ref	Expression
wph	wff 𝜑
wps	wff 𝜓
vx	setvar 𝑥

Assertion

Ref	Expression
walsi	wff ∀!𝑥(𝜑 → 𝜓)

See definition df-alsi 13954 for more information.