Theorem nrex 3065

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  rex0  4300  iun0  5004  canth  7321  orduninsuc  7794  wofib  9460  cfsuc  10179  nominpos  12414  nnunb  12433  indstr  12866  eirr  16172  sqrt2irr  16216  vdwap0  16947  smndex1n0mnd  18883  smndex2dnrinv  18886  psgnunilem3  19471  bwth  23375  zfbas  23861  aaliou3lem9  26316  vma1  27129  muls01  28104  mulsrid  28105  onmulscl  28270  hatomistici  32433  esumrnmpt2  34212  fmlan0  35573  linedegen  36325  limsucncmpi  36627  ttcwf2  36707  mh-inf3sn  36724  elpadd0  40255  rexanuz2nf  45920  fourierdlem62  46596  etransc  46711  cjnpoly  47337  0nodd  48646  2nodd  48648  1neven  48714