Theorem nrex 3272

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3141  ∃wrex 3142

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 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  rex0  4320  iun0  4988  canth  7114  orduninsuc  7561  wfrlem16  7973  wofib  9012  cfsuc  9682  nominpos  11877  nnunb  11896  indstr  12319  eirr  15561  sqrt2irr  15605  vdwap0  16315  smndex1n0mnd  18080  smndex2dnrinv  18083  psgnunilem3  18627  bwth  22021  zfbas  22507  aaliou3lem9  24942  vma1  25746  hatomistici  30142  esumrnmpt2  31331  fmlan0  32642  linedegen  33608  limsucncmpi  33797  elpadd0  36949  fourierdlem62  42460  etransc  42575  0nodd  44084  2nodd  44086  1neven  44210