Theorem nrex 3057

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

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 3045  df-rex 3054

This theorem is referenced by:  rex0  4307  iun0  5007  canth  7294  orduninsuc  7767  wofib  9425  cfsuc  10139  nominpos  12349  nnunb  12368  indstr  12805  eirr  16101  sqrt2irr  16145  vdwap0  16875  smndex1n0mnd  18773  smndex2dnrinv  18776  psgnunilem3  19362  bwth  23279  zfbas  23765  aaliou3lem9  26239  vma1  27057  muls01  28005  mulsrid  28006  onmulscl  28165  hatomistici  32293  esumrnmpt2  34049  fmlan0  35381  linedegen  36134  limsucncmpi  36436  elpadd0  39805  rexanuz2nf  45487  fourierdlem62  46163  etransc  46278  cjnpoly  46887  0nodd  48168  2nodd  48170  1neven  48236