Theorem ralsanmo

Description: An "all some" statement restricted to a class, conjoined with the claim that at most one x in A satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one x in A satisfies the antecedent. This is the restricted counterpart of alsanmo . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	ralsanmo	$$⊢\left(\forall \exists x\in A\left(\phi \to \psi \right)\wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-rals	$$⊢\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)$$
2	1	anbi1i	$$⊢\left(\forall \exists x\in A\left(\phi \to \psi \right)\wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists x\in A\phi \right)\wedge {\exists }^{*}x\in A\phi \right)$$
3		anass	$$⊢\left(\left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists x\in A\phi \right)\wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)\right)$$
4		reu5	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)$$
5	4	bicomi	$$⊢\left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \exists !x\in A\phi$$
6	5	anbi2i	$$⊢\left(\forall x\in A\left(\phi \to \psi \right)\wedge \left(\exists x\in A\phi \wedge {\exists }^{*}x\in A\phi \right)\right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)$$
7	2 3 6	3bitri	$$⊢\left(\forall \exists x\in A\left(\phi \to \psi \right)\wedge {\exists }^{*}x\in A\phi \right)\leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists !x\in A\phi \right)$$