Theorem alsraln0

Description: The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and A is not empty. (Contributed by Peter Mazsa, 28-Nov-2018) (Revised by David A. Wheeler, 15-Jul-2026)

	Ref	Expression
Assertion	alsraln0	$$⊢\forall \exists x\left(x\in A\to \phi \right)\leftrightarrow \left(\forall x\in A\phi \wedge A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		alsralrex	$$⊢\forall \exists x\left(x\in A\to \phi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \exists x\in A\phi \right)$$
2		rexn0	$$⊢\exists x\in A\phi \to A\ne \varnothing$$
3	2	a1i	$$⊢\forall x\in A\phi \to \left(\exists x\in A\phi \to A\ne \varnothing \right)$$
4		r19.2z	$$⊢\left(A\ne \varnothing \wedge \forall x\in A\phi \right)\to \exists x\in A\phi$$
5	4	expcom	$$⊢\forall x\in A\phi \to \left(A\ne \varnothing \to \exists x\in A\phi \right)$$
6	3 5	impbid	$$⊢\forall x\in A\phi \to \left(\exists x\in A\phi \leftrightarrow A\ne \varnothing \right)$$
7	6	pm5.32i	$$⊢\left(\forall x\in A\phi \wedge \exists x\in A\phi \right)\leftrightarrow \left(\forall x\in A\phi \wedge A\ne \varnothing \right)$$
8	1 7	bitri	$$⊢\forall \exists x\left(x\in A\to \phi \right)\leftrightarrow \left(\forall x\in A\phi \wedge A\ne \varnothing \right)$$