Theorem nrex 3061

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  rex0  4309  iun0  5012  canth  7306  orduninsuc  7779  wofib  9438  cfsuc  10155  nominpos  12365  nnunb  12384  indstr  12816  eirr  16116  sqrt2irr  16160  vdwap0  16890  smndex1n0mnd  18822  smndex2dnrinv  18825  psgnunilem3  19410  bwth  23326  zfbas  23812  aaliou3lem9  26286  vma1  27104  muls01  28052  mulsrid  28053  onmulscl  28212  hatomistici  32344  esumrnmpt2  34102  fmlan0  35456  linedegen  36208  limsucncmpi  36510  elpadd0  39928  rexanuz2nf  45614  fourierdlem62  46290  etransc  46405  cjnpoly  47013  0nodd  48294  2nodd  48296  1neven  48362