Theorem nrex 3196

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064

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

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

This theorem is referenced by:  rex0  4288  iun0  4987  canth  7209  orduninsuc  7665  wfrlem16OLD  8126  wofib  9234  cfsuc  9944  nominpos  12140  nnunb  12159  indstr  12585  eirr  15842  sqrt2irr  15886  vdwap0  16605  smndex1n0mnd  18466  smndex2dnrinv  18469  psgnunilem3  19019  bwth  22469  zfbas  22955  aaliou3lem9  25415  vma1  26220  hatomistici  30625  esumrnmpt2  31936  fmlan0  33253  linedegen  34372  limsucncmpi  34561  elpadd0  37750  fourierdlem62  43599  etransc  43714  0nodd  45252  2nodd  45254  1neven  45378