Theorem nrex 3269

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139

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 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  rex0  4316  iun0  4977  canth  7105  orduninsuc  7552  wfrlem16  7964  wofib  9003  cfsuc  9673  nominpos  11868  nnunb  11887  indstr  12310  eirr  15552  sqrt2irr  15596  vdwap0  16306  smndex1n0mnd  18071  smndex2dnrinv  18074  psgnunilem3  18618  bwth  22012  zfbas  22498  aaliou3lem9  24933  vma1  25737  hatomistici  30133  esumrnmpt2  31322  fmlan0  32633  linedegen  33599  limsucncmpi  33788  elpadd0  36939  fourierdlem62  42447  etransc  42562  0nodd  44071  2nodd  44073  1neven  44197