Theorem rext0

Description: Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	rext0.1	$$⊢\phi$$
Assertion	rext0	$$⊢\exists x\in A\phi \leftrightarrow A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rext0.1	$$⊢\phi$$
2	1	notnoti	$$⊢\neg \neg \phi$$
3	2	ralf0	$$⊢\forall x\in A\neg \phi \leftrightarrow A=\varnothing$$
4	3	notbii	$$⊢\neg \forall x\in A\neg \phi \leftrightarrow \neg A=\varnothing$$
5		dfrex2	$$⊢\exists x\in A\phi \leftrightarrow \neg \forall x\in A\neg \phi$$
6		df-ne	$$⊢A\ne \varnothing \leftrightarrow \neg A=\varnothing$$
7	4 5 6	3bitr4i	$$⊢\exists x\in A\phi \leftrightarrow A\ne \varnothing$$