Theorem nrex 3066

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  rex0  4314  iun0  5019  canth  7322  orduninsuc  7795  wofib  9462  cfsuc  10179  nominpos  12390  nnunb  12409  indstr  12841  eirr  16142  sqrt2irr  16186  vdwap0  16916  smndex1n0mnd  18849  smndex2dnrinv  18852  psgnunilem3  19437  bwth  23366  zfbas  23852  aaliou3lem9  26326  vma1  27144  muls01  28120  mulsrid  28121  onmulscl  28286  hatomistici  32449  esumrnmpt2  34245  fmlan0  35604  linedegen  36356  limsucncmpi  36658  elpadd0  40179  rexanuz2nf  45844  fourierdlem62  46520  etransc  46635  cjnpoly  47243  0nodd  48524  2nodd  48526  1neven  48592