Definition df-alseu 50599

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 50597	. 2 wff ∀∃!𝑥(𝜑 → 𝜓)
5	1, 2	wi 4	. . . 4 wff (𝜑 → 𝜓)
6	5, 3	wal 1568	. . 3 wff ∀𝑥(𝜑 → 𝜓)
7	1, 3	weu 2596	. . 3 wff ∃!𝑥𝜑
8	6, 7	wa 400	. 2 wff (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑)
9	4, 8	wb 209	1 wff (∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))

This definition is referenced by:  dfralseu2  50601  alseuals  50602  alseud  50604  alseu1d  50606  alseu2d  50607  alseubii  50610  nfalseu  50612  dfalseu2  50614