Theorem nrex 3092

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3079  df-rex 3089

This theorem is used by:  rex0  4311  iun0  5024  canth  7371  orduninsuc  7843  wofib  9521  cfsuc  10263  nominpos  12509  nnunb  12528  indstr  12969  eirr  16299  sqrt2irr  16343  vdwap0  17074  smndex1n0mnd  19030  smndex2dnrinv  19033  psgnunilem3  19629  bwth  23641  zfbas  24128  aaliou3lem9  26593  vma1  27410  muls01  28385  mulsrid  28386  onmulscl  28551  hatomistici  32851  esumrnmpt2  34586  fmlan0  35978  linedegen  36731  limsucncmpi  37072  ttcwf2  37152  mh-inf3sn  37169  elpadd0  40690  rexanuz2nf  46328  fourierdlem62  47004  etransc  47119  cjnpoly  47765  0nodd  49093  2nodd  49095  1neven  49161