Definition df-alsc 10118

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

Assertion

Ref	Expression
df-alsc	⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))

Detailed syntax breakdown of Definition df-alsc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	walsc 10116	. 2 wff ∀!𝑥 ∈ 𝐴𝜑
5	1, 2, 3	wral 2306	. . 3 wff ∀𝑥 ∈ 𝐴 𝜑
6	2	cv 1242	. . . . 5 class 𝑥
7	6, 3	wcel 1393	. . . 4 wff 𝑥 ∈ 𝐴
8	7, 2	wex 1381	. . 3 wff ∃𝑥 𝑥 ∈ 𝐴
9	5, 8	wa 97	. 2 wff (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴)
10	4, 9	wb 98	1 wff (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))

This definition is referenced by:  alsconv  10119  alsc1d  10122  alsc2d  10123