Theorem nrex 3096

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3083  df-rex 3093

This theorem is used by:  rex0  4318  iun0  5031  canth  7377  orduninsuc  7848  wofib  9517  cfsuc  10259  nominpos  12499  nnunb  12518  indstr  12958  eirr  16286  sqrt2irr  16330  vdwap0  17061  smndex1n0mnd  19005  smndex2dnrinv  19008  psgnunilem3  19597  bwth  23604  zfbas  24090  aaliou3lem9  26550  vma1  27367  muls01  28342  mulsrid  28343  onmulscl  28508  hatomistici  32751  esumrnmpt2  34489  fmlan0  35903  linedegen  36655  limsucncmpi  36996  ttcwf2  37076  mh-inf3sn  37093  elpadd0  40623  rexanuz2nf  46246  fourierdlem62  46922  etransc  47037  cjnpoly  47666  0nodd  48975  2nodd  48977  1neven  49043