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	⊢ ( ∀! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3	2 0 1	walsc	⊢ ∀! 𝑥 ∈ 𝐴 𝜑
4	2 0 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 𝜑
5	0	cv	⊢ 𝑥
6	5 1	wcel	⊢ 𝑥 ∈ 𝐴
7	6 0	wex	⊢ ∃ 𝑥 𝑥 ∈ 𝐴
8	4 7	wa	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 )
9	3 8	wb	⊢ ( ∀! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) )