Definition df-alseu

Description: Define "all some one" applied to a top-level implication, which means ps is true whenever ph is true and exactly one x satisfies ph . (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Assertion	df-alseu	$$⊢\forall \exists !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	walseu	$$wff\forall \exists !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	weu	$$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 \exists !x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\left(\phi \to \psi \right)\wedge \exists !x\phi \right)\right)$$