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

Theorem nrex 2997
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 2919 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 2989 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 220 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1988  wral 2909  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-ral 2914  df-rex 2915
This theorem is referenced by:  rex0  3930  iun0  4567  canth  6593  orduninsuc  7028  wfrlem16  7415  wofib  8435  cfsuc  9064  nominpos  11254  nnunb  11273  indstr  11741  eirr  14914  sqrt2irr  14960  vdwap0  15661  psgnunilem3  17897  bwth  21194  zfbas  21681  aaliou3lem9  24086  vma1  24873  hatomistici  29191  esumrnmpt2  30104  linedegen  32225  limsucncmpi  32419  elpadd0  34914  fourierdlem62  40148  etransc  40263  0nodd  41575  2nodd  41577  1neven  41697
  Copyright terms: Public domain W3C validator