Definition df-alsc

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)

	Ref	Expression
Assertion	df-alsc	$$⊢\forall !x\in A\phi \leftrightarrow \left(\forall x\in A\phi \wedge \exists xx\in A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	walsc	$$wff\forall !x\in A\phi$$
4	2 0 1	wral	$$wff\forall x\in A\phi$$
5	0	cv	$$setvarx$$
6	5 1	wcel	$$wffx\in A$$
7	6 0	wex	$$wff\exists xx\in A$$
8	4 7	wa	$$wff\left(\forall x\in A\phi \wedge \exists xx\in A\right)$$
9	3 8	wb	$$wff\left(\forall !x\in A\phi \leftrightarrow \left(\forall x\in A\phi \wedge \exists xx\in A\right)\right)$$