Theorem nrex 3060

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  rex0  4310  iun0  5010  canth  7300  orduninsuc  7773  wofib  9431  cfsuc  10145  nominpos  12355  nnunb  12374  indstr  12811  eirr  16111  sqrt2irr  16155  vdwap0  16885  smndex1n0mnd  18817  smndex2dnrinv  18820  psgnunilem3  19406  bwth  23323  zfbas  23809  aaliou3lem9  26283  vma1  27101  muls01  28049  mulsrid  28050  onmulscl  28209  hatomistici  32337  esumrnmpt2  34076  fmlan0  35423  linedegen  36176  limsucncmpi  36478  elpadd0  39847  rexanuz2nf  45529  fourierdlem62  46205  etransc  46320  cjnpoly  46919  0nodd  48200  2nodd  48202  1neven  48268