Theorem nrexdv

Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003) (Proof shortened by Wolf Lammen, 5-Jan-2020)

	Ref	Expression
Hypothesis	nrexdv.1	$$⊢\left(\phi \wedge x\in A\right)\to \neg \psi$$
Assertion	nrexdv	$$⊢\phi \to \neg \exists x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		nrexdv.1	$$⊢\left(\phi \wedge x\in A\right)\to \neg \psi$$
2	1	ralrimiva	$$⊢\phi \to \forall x\in A\neg \psi$$
3		ralnex	$$⊢\forall x\in A\neg \psi \leftrightarrow \neg \exists x\in A\psi$$
4	2 3	sylib	$$⊢\phi \to \neg \exists x\in A\psi$$