Theorem nrex 3057

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

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 3045  df-rex 3054

This theorem is referenced by:  rex0  4323  iun0  5026  canth  7341  orduninsuc  7819  wofib  9498  cfsuc  10210  nominpos  12419  nnunb  12438  indstr  12875  eirr  16173  sqrt2irr  16217  vdwap0  16947  smndex1n0mnd  18839  smndex2dnrinv  18842  psgnunilem3  19426  bwth  23297  zfbas  23783  aaliou3lem9  26258  vma1  27076  muls01  28015  mulsrid  28016  onmulscl  28175  hatomistici  32291  esumrnmpt2  34058  fmlan0  35378  linedegen  36131  limsucncmpi  36433  elpadd0  39803  rexanuz2nf  45488  fourierdlem62  46166  etransc  46281  cjnpoly  46890  0nodd  48158  2nodd  48160  1neven  48226