This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝜓 )
	Assertion	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nrexdv.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝜓 )
2	1	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 )
3		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )
4	2 3	sylib	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐴 𝜓 )