Theorem nrex 3074

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

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

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 3062  df-rex 3071

This theorem is referenced by:  rex0  4360  iun0  5062  canth  7385  orduninsuc  7864  wfrlem16OLD  8364  wofib  9585  cfsuc  10297  nominpos  12503  nnunb  12522  indstr  12958  eirr  16241  sqrt2irr  16285  vdwap0  17014  smndex1n0mnd  18925  smndex2dnrinv  18928  psgnunilem3  19514  bwth  23418  zfbas  23904  aaliou3lem9  26392  vma1  27209  muls01  28138  mulsrid  28139  onmulscl  28287  hatomistici  32381  esumrnmpt2  34069  fmlan0  35396  linedegen  36144  limsucncmpi  36446  elpadd0  39811  rexanuz2nf  45503  fourierdlem62  46183  etransc  46298  0nodd  48086  2nodd  48088  1neven  48154