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

Theorem nrex 2658
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 2621 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2566 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3mpbi 199 1  |-  -.  E. x  e.  A  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1696   A.wral 2556   E.wrex 2557
This theorem is referenced by:  rex0  3481  iun0  3974  orduninsuc  4650  canth  6310  wofib  7276  cfsuc  7899  nominpos  9964  nnunb  9977  indstr  10303  eirr  12499  sqr2irr  12543  vdwap0  13039  zfbas  17607  aaliou3lem9  19746  vma1  20420  hatomistici  22958  wfrlem16  24342  linedegen  24838  limsucncmpi  24956  psgnunilem3  27522  elpadd0  30620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator