Definition df-alsi

Description: Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2		wps	|- ps
3	1 2 0	walsi	|- A! x ( ph -> ps )
4	1 2	wi	|- ( ph -> ps )
5	4 0	wal	|- A. x ( ph -> ps )
6	1 0	wex	|- E. x ph
7	5 6	wa	|- ( A. x ( ph -> ps ) /\ E. x ph )
8	3 7	wb	|- ( A! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )