Theorem n0als

Description: If A is not empty, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that ph holds for every x in A . (Contributed by Peter Mazsa, 19-Dec-2018) (Revised by David A. Wheeler, 15-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		alsraln0	$$⊢\forall \exists x\left(x\in A\to \phi \right)\leftrightarrow \left(\forall x\in A\phi \wedge A\ne \varnothing \right)$$
2	1	rbaib	$$⊢A\ne \varnothing \to \left(\forall \exists x\left(x\in A\to \phi \right)\leftrightarrow \forall x\in A\phi \right)$$