Syntax Definition wrals 50445

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

Hypotheses

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

Assertion

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

See definition df-rals 50447 for more information.