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

Theorem nrex 2645
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 2608 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2553 . 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 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  rex0  3468  iun0  3958  orduninsuc  4634  canth  6294  wofib  7260  cfsuc  7883  nominpos  9948  nnunb  9961  indstr  10287  eirr  12483  sqr2irr  12527  vdwap0  13023  zfbas  17591  aaliou3lem9  19730  vma1  20404  hatomistici  22942  wfrlem16  24271  linedegen  24766  limsucncmpi  24884  psgnunilem3  27419  elpadd0  29998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator