Definition df-als

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-als	Could not format assertion : No typesetting found for |- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2		wps	$$wff\psi$$
3	1 2 0	wals	Could not format AE x ( ph -> ps ) : No typesetting found for wff AE x ( ph -> ps ) with typecode wff
4	1 2	wi	$$wff\left(\phi \to \psi \right)$$
5	4 0	wal	$$wff\forall x\left(\phi \to \psi \right)$$
6	1 0	wex	$$wff\exists x\phi$$
7	5 6	wa	$$wff\left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \right)$$
8	3 7	wb	Could not format ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) ) : No typesetting found for wff ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) ) with typecode wff