Theorem ralrals

Description: If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of A satisfying its antecedent. This is the restricted counterpart of ralals . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	ralrals	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\forall \exists x\in A\left(\phi \to \psi \right)\leftrightarrow \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		ibar	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\exists x\in A\phi \leftrightarrow \left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists x\in A\phi \right)\right)$$
3	2	bicomd	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\left(\forall x\in A\left(\phi \to \psi \right)\wedge \exists x\in A\phi \right)\leftrightarrow \exists x\in A\phi \right)$$
4	1 3	bitrid	$$⊢\forall x\in A\left(\phi \to \psi \right)\to \left(\forall \exists x\in A\left(\phi \to \psi \right)\leftrightarrow \exists x\in A\phi \right)$$