Theorem nrex 3069

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2099  ∀wral 3056  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-ral 3057  df-rex 3066

This theorem is referenced by:  rex0  4353  iun0  5059  canth  7367  orduninsuc  7839  wfrlem16OLD  8336  wofib  9554  cfsuc  10266  nominpos  12465  nnunb  12484  indstr  12916  eirr  16167  sqrt2irr  16211  vdwap0  16930  smndex1n0mnd  18849  smndex2dnrinv  18852  psgnunilem3  19435  bwth  23288  zfbas  23774  aaliou3lem9  26259  vma1  27072  muls01  27986  mulsrid  27987  hatomistici  32146  esumrnmpt2  33610  fmlan0  34924  linedegen  35662  limsucncmpi  35852  elpadd0  39206  rexanuz2nf  44788  fourierdlem62  45469  etransc  45584  0nodd  47145  2nodd  47147  1neven  47213