Definition df-als 17335

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

Assertion

Ref	Expression
df-als	⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))

Detailed syntax breakdown of Definition df-als

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		vx	. . 3 setvar 𝑥
4	1, 2, 3	wals 17333	. 2 wff ∀∃𝑥(𝜑 → 𝜓)
5	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
6	5, 3	wal 1400	. . 3 wff ∀𝑥(𝜑 → 𝜓)
7	1, 3	wex 1545	. . 3 wff ∃𝑥𝜑
8	6, 7	wa 104	. 2 wff (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑)
9	4, 8	wb 105	1 wff (∀∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))

This definition is used by:  dfrals2  17337  alsd  17338  als1d  17340  als2d  17341  alsex  17346  alsbii  17348  alsbid  17350  nfals  17351  cbvals  17353  als-no-surprise  17354  alsanmo  17358  alsralrex  17360  alsraln0m  17361  alseuals  17372