Theorem nrex

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

	Ref	Expression
Hypothesis	nrex.1	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 )
Assertion	nrex	⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝜓

Proof

Step	Hyp	Ref	Expression
1		nrex.1	⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 )
2	1	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓
3		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )
4	2 3	mpbi	⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝜓