Theorem nrex 3080

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  rex0  4383  iun0  5085  canth  7401  orduninsuc  7880  wfrlem16OLD  8380  wofib  9614  cfsuc  10326  nominpos  12530  nnunb  12549  indstr  12981  eirr  16253  sqrt2irr  16297  vdwap0  17023  smndex1n0mnd  18947  smndex2dnrinv  18950  psgnunilem3  19538  bwth  23439  zfbas  23925  aaliou3lem9  26410  vma1  27227  muls01  28156  mulsrid  28157  onmulscl  28305  hatomistici  32394  esumrnmpt2  34032  fmlan0  35359  linedegen  36107  limsucncmpi  36411  elpadd0  39766  rexanuz2nf  45408  fourierdlem62  46089  etransc  46204  0nodd  47893  2nodd  47895  1neven  47961