Theorem nrex 3074

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 3063	. 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓
3		ralnex 3072	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbi 229	1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3062  df-rex 3071

This theorem is referenced by:  rex0  4356  iun0  5064  canth  7358  orduninsuc  7828  wfrlem16OLD  8320  wofib  9536  cfsuc  10248  nominpos  12445  nnunb  12464  indstr  12896  eirr  16144  sqrt2irr  16188  vdwap0  16905  smndex1n0mnd  18789  smndex2dnrinv  18792  psgnunilem3  19358  bwth  22905  zfbas  23391  aaliou3lem9  25854  vma1  26659  muls01  27557  mulsrid  27558  hatomistici  31602  esumrnmpt2  33054  fmlan0  34370  linedegen  35103  limsucncmpi  35318  elpadd0  38668  rexanuz2nf  44189  fourierdlem62  44870  etransc  44985  0nodd  46566  2nodd  46568  1neven  46783