Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nrex Structured version   Visualization version   GIF version

Theorem nrex 3231
 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
StepHypRef Expression
1 nrex.1 . . 3 (𝑥𝐴 → ¬ 𝜓)
21rgen 3119 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 3202 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 233 1 ¬ ∃𝑥𝐴 𝜓
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2112  ∀wral 3109  ∃wrex 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115 This theorem is referenced by:  rex0  4274  iun0  4951  canth  7094  orduninsuc  7542  wfrlem16  7957  wofib  8997  cfsuc  9672  nominpos  11866  nnunb  11885  indstr  12308  eirr  15553  sqrt2irr  15597  vdwap0  16305  smndex1n0mnd  18072  smndex2dnrinv  18075  psgnunilem3  18619  bwth  22018  zfbas  22504  aaliou3lem9  24949  vma1  25754  hatomistici  30148  esumrnmpt2  31435  fmlan0  32746  linedegen  33712  limsucncmpi  33901  elpadd0  37098  fourierdlem62  42797  etransc  42912  0nodd  44417  2nodd  44419  1neven  44543
 Copyright terms: Public domain W3C validator