Theorem rexn0

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) Avoid df-clel , ax-8 . (Revised by GG, 2-Sep-2024)

	Ref	Expression
Assertion	rexn0	$$⊢\exists x\in A\phi \to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dfrex2	$$⊢\exists x\in A\phi \leftrightarrow \neg \forall x\in A\neg \phi$$
2		rzal	$$⊢A=\varnothing \to \forall x\in A\neg \phi$$
3	2	con3i	$$⊢\neg \forall x\in A\neg \phi \to \neg A=\varnothing$$
4	1 3	sylbi	$$⊢\exists x\in A\phi \to \neg A=\varnothing$$
5	4	neqned	$$⊢\exists x\in A\phi \to A\ne \varnothing$$