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  4313  iun0  5014  canth  7307  orduninsuc  7783  wofib  9456  cfsuc  10170  nominpos  12379  nnunb  12398  indstr  12835  eirr  16132  sqrt2irr  16176  vdwap0  16906  smndex1n0mnd  18804  smndex2dnrinv  18807  psgnunilem3  19393  bwth  23313  zfbas  23799  aaliou3lem9  26274  vma1  27092  muls01  28038  mulsrid  28039  onmulscl  28198  hatomistici  32324  esumrnmpt2  34034  fmlan0  35363  linedegen  36116  limsucncmpi  36418  elpadd0  39788  rexanuz2nf  45472  fourierdlem62  46150  etransc  46265  cjnpoly  46874  0nodd  48155  2nodd  48157  1neven  48223