Theorem nrex 3072

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  rex0  4366  iun0  5067  canth  7385  orduninsuc  7864  wfrlem16OLD  8363  wofib  9583  cfsuc  10295  nominpos  12501  nnunb  12520  indstr  12956  eirr  16238  sqrt2irr  16282  vdwap0  17010  smndex1n0mnd  18938  smndex2dnrinv  18941  psgnunilem3  19529  bwth  23434  zfbas  23920  aaliou3lem9  26407  vma1  27224  muls01  28153  mulsrid  28154  onmulscl  28302  hatomistici  32391  esumrnmpt2  34049  fmlan0  35376  linedegen  36125  limsucncmpi  36428  elpadd0  39792  rexanuz2nf  45443  fourierdlem62  46124  etransc  46239  0nodd  48014  2nodd  48016  1neven  48082