Theorem nrex 3072

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2101  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1778  df-ral 3060  df-rex 3069

This theorem is referenced by:  rex0  4294  iun0  4994  canth  7249  orduninsuc  7710  wfrlem16OLD  8175  wofib  9332  cfsuc  10041  nominpos  12238  nnunb  12257  indstr  12684  eirr  15942  sqrt2irr  15986  vdwap0  16705  smndex1n0mnd  18579  smndex2dnrinv  18582  psgnunilem3  19132  bwth  22589  zfbas  23075  aaliou3lem9  25538  vma1  26343  hatomistici  30752  esumrnmpt2  32064  fmlan0  33381  linedegen  34473  limsucncmpi  34662  elpadd0  37849  fourierdlem62  43744  etransc  43859  0nodd  45404  2nodd  45406  1neven  45530