Theorem nrex

Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003)

	Ref	Expression
Hypothesis	nrex.1	$$⊢x\in A\to \neg \psi$$
Assertion	nrex	$$⊢\neg \exists x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		nrex.1	$$⊢x\in A\to \neg \psi$$
2	1	rgen	$$⊢\forall x\in A\neg \psi$$
3		ralnex	$$⊢\forall x\in A\neg \psi \leftrightarrow \neg \exists x\in A\psi$$
4	2 3	mpbi	$$⊢\neg \exists x\in A\psi$$