Theorem nrex 3090

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  rex0  4307  iun0  5019  canth  7374  orduninsuc  7854  wofib  9542  cfsuc  10338  nominpos  12586  nnunb  12605  indstr  13046  eirr  16378  sqrt2irr  16422  vdwap0  17159  smndex1n0mnd  19116  smndex2dnrinv  19119  psgnunilem3  19715  bwth  23733  zfbas  24220  aaliou3lem9  26682  vma1  27498  muls01  28503  mulsrid  28504  onmulscl  28669  hatomistici  32969  esumrnmpt2  34746  fmlan0  36242  linedegen  37000  limsucncmpi  37325  ttcwf2  37405  mh-inf3sn  37422  elpadd0  40959  rexanuz2nf  46595  fourierdlem62  47271  etransc  47386  cjnpoly  48032  0nodd  49360  2nodd  49362  1neven  49428