Theorem nrex 3000

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

Hypothesis

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

Assertion

Ref	Expression
nrex	⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓

Proof of Theorem nrex

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rex0  3938  iun0  4576  canth  6608  orduninsuc  7043  wfrlem16  7430  wofib  8450  cfsuc  9079  nominpos  11269  nnunb  11288  indstr  11756  eirr  14933  sqrt2irr  14979  vdwap0  15680  psgnunilem3  17916  bwth  21213  zfbas  21700  aaliou3lem9  24105  vma1  24892  hatomistici  29221  esumrnmpt2  30130  linedegen  32250  limsucncmpi  32444  elpadd0  35095  fourierdlem62  40385  etransc  40500  0nodd  41810  2nodd  41812  1neven  41932