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

Theorem nrex 2887
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 2792 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2878 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3mpbi 211 1  |-  -.  E. x  e.  A  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1870   A.wral 2782   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  rex0  3782  iun0  4358  canth  6264  orduninsuc  6684  wfrlem16  7059  wofib  8060  cfsuc  8685  nominpos  10849  nnunb  10865  indstr  11227  eirr  14235  sqrt2irr  14279  vdwap0  14889  psgnunilem3  17088  bwth  20356  zfbas  20842  aaliou3lem9  23171  vma1  23956  hatomistici  27850  esumrnmpt2  28728  linedegen  30695  limsucncmpi  30890  elpadd0  33083  fourierdlem62  37600  etransc  37715  0nodd  38577  2nodd  38579  1neven  38699
  Copyright terms: Public domain W3C validator