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

Theorem nrex 2919
Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
Hypothesis
Ref Expression
nrex.1  |-  ( x  e.  A  ->  -.  ps )
Assertion
Ref Expression
nrex  |-  -.  E. x  e.  A  ps

Proof of Theorem nrex
StepHypRef Expression
1 nrex.1 . . 3  |-  ( x  e.  A  ->  -.  ps )
21rgen 2824 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2910 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3mpbi 208 1  |-  -.  E. x  e.  A  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1767   A.wral 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  rex0  3799  iun0  4381  canth  6242  orduninsuc  6662  wofib  7970  cfsuc  8637  nominpos  10775  nnunb  10791  indstr  11150  eirr  13799  sqrt2irr  13843  vdwap0  14353  psgnunilem3  16327  bwth  19704  zfbas  20160  aaliou3lem9  22508  vma1  23196  hatomistici  26985  wfrlem16  28963  linedegen  29398  limsucncmpi  29515  elpadd0  34623
  Copyright terms: Public domain W3C validator