Theorem nrex 2983

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  rex0  3894  iun0  4512  canth  6508  orduninsuc  6935  wfrlem16  7317  wofib  8333  cfsuc  8962  nominpos  11146  nnunb  11165  indstr  11632  eirr  14772  sqrt2irr  14817  vdwap0  15518  psgnunilem3  17739  bwth  21023  zfbas  21510  aaliou3lem9  23909  vma1  24692  hatomistici  28605  esumrnmpt2  29457  linedegen  31420  limsucncmpi  31614  elpadd0  34113  fourierdlem62  39061  etransc  39176  0nodd  41600  2nodd  41602  1neven  41722