Definition df-alseu

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, 21-Jul-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2		wps	|- ps
3	1 2 0	walseu	|- AE! x ( ph -> ps )
4	1 2	wi	|- ( ph -> ps )
5	4 0	wal	|- A. x ( ph -> ps )
6	1 0	weu	|- E! x ph
7	5 6	wa	|- ( A. x ( ph -> ps ) /\ E! x ph )
8	3 7	wb	|- ( AE! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )