Definition df-alsc 42535

Description: Define "all some" applied to a class, which means ph is true for all x in A and there is at least one x in A. (Contributed by David A. Wheeler, 20-Oct-2018.)

Assertion

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

Detailed syntax breakdown of Definition df-alsc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	walsc 42533	. 2 wff A.! x e. A ph
5	1, 2, 3	wral 2912	. . 3 wff A. x e. A ph
6	2	cv 1482	. . . . 5 class x
7	6, 3	wcel 1990	. . . 4 wff x e. A
8	7, 2	wex 1704	. . 3 wff E. x x e. A
9	5, 8	wa 384	. 2 wff ( A. x e. A ph /\ E. x x e. A )
10	4, 9	wb 196	1 wff ( A.! x e. A ph <-> ( A. x e. A ph /\ E. x x e. A ) )

This definition is referenced by:  alsconv  42536  alsc1d  42539  alsc2d  42540