Definition df-ralseu 17137

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

Assertion

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

Detailed syntax breakdown of Definition df-ralseu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		vx	. . 3 setvar x
4		cA	. . 3 class A
5	1, 2, 3, 4	wralseu 17135	. 2 wff A.E! x e. A ( ph -> ps )
6	1, 2	wi 4	. . . 4 wff ( ph -> ps )
7	6, 3, 4	wral 2528	. . 3 wff A. x e. A ( ph -> ps )
8	1, 3, 4	wreu 2530	. . 3 wff E! x e. A ph
9	7, 8	wa 104	. 2 wff ( A. x e. A ( ph -> ps ) /\ E! x e. A ph )
10	5, 9	wb 105	1 wff ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )

This definition is referenced by:  dfralseu2  17138  ralseurals  17140  ralseud  17142  ralseu1d  17145  ralseu2d  17146  ralseubii  17148  nfralseu  17150