Theorem nrex 3089

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  rex0  4312  iun0  5018  canth  7346  orduninsuc  7819  wofib  9490  cfsuc  10211  nominpos  12455  nnunb  12474  indstr  12914  eirr  16220  sqrt2irr  16264  vdwap0  16995  smndex1n0mnd  18932  smndex2dnrinv  18935  psgnunilem3  19519  bwth  23450  zfbas  23936  aaliou3lem9  26391  vma1  27207  muls01  28182  mulsrid  28183  onmulscl  28348  hatomistici  32511  esumrnmpt2  34326  fmlan0  35705  linedegen  36457  limsucncmpi  36769  ttcwf2  36849  mh-inf3sn  36866  elpadd0  40397  rexanuz2nf  46030  fourierdlem62  46706  etransc  46821  cjnpoly  47447  0nodd  48756  2nodd  48758  1neven  48824