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	$$⊢\forall !x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2		wps	$$wff\psi$$
3	1 2 0	walsi	$$wff\forall !x\left(\phi \to \psi \right)$$
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	$$wff\left(\forall !x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\left(\phi \to \psi \right)\wedge \exists x\phi \right)\right)$$