Theorem nrex 3068

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

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

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  rex0  4295  iun0  4998  canth  7317  orduninsuc  7790  wofib  9457  cfsuc  10177  nominpos  12412  nnunb  12431  indstr  12864  eirr  16170  sqrt2irr  16214  vdwap0  16945  smndex1n0mnd  18881  smndex2dnrinv  18884  psgnunilem3  19469  bwth  23400  zfbas  23886  aaliou3lem9  26341  vma1  27154  muls01  28129  mulsrid  28130  onmulscl  28295  hatomistici  32458  esumrnmpt2  34259  fmlan0  35626  linedegen  36378  limsucncmpi  36680  ttcwf2  36760  mh-inf3sn  36777  elpadd0  40308  rexanuz2nf  45942  fourierdlem62  46618  etransc  46733  cjnpoly  47359  0nodd  48668  2nodd  48670  1neven  48736