Definition df-alseu 17174

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

Assertion

Ref	Expression
df-alseu	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )

Detailed syntax breakdown of Definition df-alseu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		vx	. . 3 setvar x
4	1, 2, 3	walseu 17172	. 2 wff A.E! x ( ph -> ps )
5	1, 2	wi 4	. . . 4 wff ( ph -> ps )
6	5, 3	wal 1400	. . 3 wff A. x ( ph -> ps )
7	1, 3	weu 2086	. . 3 wff E! x ph
8	6, 7	wa 104	. 2 wff ( A. x ( ph -> ps ) /\ E! x ph )
9	4, 8	wb 105	1 wff ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )

This definition is used by:  dfralseu2  17176  alseuals  17177  alseud  17179  alseu1d  17181  alseu2d  17182  alseubii  17185  nfalseu  17187  dfalseu2  17189