Definition df-als 17226

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.)

Assertion

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

Detailed syntax breakdown of Definition df-als

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		vx	. . 3 setvar x
4	1, 2, 3	wals 17224	. 2 wff A.E. x ( ph -> ps )
5	1, 2	wi 4	. . . 4 wff ( ph -> ps )
6	5, 3	wal 1400	. . 3 wff A. x ( ph -> ps )
7	1, 3	wex 1545	. . 3 wff E. x ph
8	6, 7	wa 104	. 2 wff ( A. x ( ph -> ps ) /\ E. x ph )
9	4, 8	wb 105	1 wff ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )

This definition is used by:  dfrals2  17228  alsd  17229  als1d  17231  als2d  17232  alsex  17237  alsbii  17239  alsbid  17241  nfals  17242  cbvals  17244  als-no-surprise  17245  alsanmo  17249  alsralrex  17251  alsraln0m  17252  alseuals  17263