Definition df-alseu 50656

Description: Define "all some one" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and exactly one 𝑥 satisfies 𝜑. (Contributed by David A. Wheeler, 21-Jul-2026.)

Assertion

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

Detailed syntax breakdown of Definition df-alseu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		vx	. . 3 setvar 𝑥
4	1, 2, 3	walseu 50654	. 2 wff ∀∃!𝑥(𝜑 → 𝜓)
5	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
6	5, 3	wal 1568	. . 3 wff ∀𝑥(𝜑 → 𝜓)
7	1, 3	weu 2598	. . 3 wff ∃!𝑥𝜑
8	6, 7	wa 401	. 2 wff (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑)
9	4, 8	wb 209	1 wff (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))

This definition is used by:  dfralseu2  50658  alseuals  50659  alseud  50661  alseu1d  50663  alseu2d  50664  alseubii  50667  nfalseu  50669  dfalseu2  50671