Definition df-ralseu

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

	Ref	Expression
Assertion	df-ralseu	$$⊢\forall \exists !x\in A\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3		wps	$$wff\psi$$
4	2 3 0 1	wralseu	$$wff\forall \exists !x\in A\left(\phi \to \psi \right)$$
5	2 3	wi	$$wff\left(\phi \to \psi \right)$$
6	5 0 1	wral	$$wff\forall x\in A\left(\phi \to \psi \right)$$
7	2 0 1	wreu	$$wff\exists !x\in A\phi$$
8	6 7	wa	$$wff\left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)$$
9	4 8	wb	$$wff\left(\forall \exists !x\in A\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)\right)$$