Theorem nrex 3064

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  rex0  4312  iun0  5017  canth  7312  orduninsuc  7785  wofib  9450  cfsuc  10167  nominpos  12378  nnunb  12397  indstr  12829  eirr  16130  sqrt2irr  16174  vdwap0  16904  smndex1n0mnd  18837  smndex2dnrinv  18840  psgnunilem3  19425  bwth  23354  zfbas  23840  aaliou3lem9  26314  vma1  27132  muls01  28108  mulsrid  28109  onmulscl  28274  hatomistici  32437  esumrnmpt2  34225  fmlan0  35585  linedegen  36337  limsucncmpi  36639  elpadd0  40065  rexanuz2nf  45732  fourierdlem62  46408  etransc  46523  cjnpoly  47131  0nodd  48412  2nodd  48414  1neven  48480