Theorem nrex 3064

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3052  df-rex 3061

This theorem is referenced by:  rex0  4335  iun0  5038  canth  7359  orduninsuc  7838  wfrlem16OLD  8338  wofib  9559  cfsuc  10271  nominpos  12478  nnunb  12497  indstr  12932  eirr  16223  sqrt2irr  16267  vdwap0  16996  smndex1n0mnd  18890  smndex2dnrinv  18893  psgnunilem3  19477  bwth  23348  zfbas  23834  aaliou3lem9  26310  vma1  27128  muls01  28067  mulsrid  28068  onmulscl  28227  hatomistici  32343  esumrnmpt2  34099  fmlan0  35413  linedegen  36161  limsucncmpi  36463  elpadd0  39828  rexanuz2nf  45519  fourierdlem62  46197  etransc  46312  0nodd  48145  2nodd  48147  1neven  48213