Theorem nrex 3091

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087

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 3078  df-rex 3088

This theorem is used by:  rex0  4308  iun0  5020  canth  7366  orduninsuc  7843  wofib  9523  cfsuc  10316  nominpos  12564  nnunb  12583  indstr  13024  eirr  16353  sqrt2irr  16397  vdwap0  17134  smndex1n0mnd  19091  smndex2dnrinv  19094  psgnunilem3  19690  bwth  23708  zfbas  24195  aaliou3lem9  26659  vma1  27475  muls01  28480  mulsrid  28481  onmulscl  28646  hatomistici  32946  esumrnmpt2  34682  fmlan0  36125  linedegen  36878  limsucncmpi  37203  ttcwf2  37283  mh-inf3sn  37300  elpadd0  40834  rexanuz2nf  46446  fourierdlem62  47122  etransc  47237  cjnpoly  47883  0nodd  49211  2nodd  49213  1neven  49279