Definition df-ralseu

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		wph	|- ph
3		wps	|- ps
4	2 3 0 1	wralseu	|- AE! x e. A ( ph -> ps )
5	2 3	wi	|- ( ph -> ps )
6	5 0 1	wral	|- A. x e. A ( ph -> ps )
7	2 0 1	wreu	|- E! x e. A ph
8	6 7	wa	|- ( A. x e. A ( ph -> ps ) /\ E! x e. A ph )
9	4 8	wb	|- ( AE! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )