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

Theorem nrex 2808
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 2771 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2715 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3mpbi 200 1  |-  -.  E. x  e.  A  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1725   A.wral 2705   E.wrex 2706
This theorem is referenced by:  rex0  3641  iun0  4147  orduninsuc  4823  canth  6539  wofib  7514  cfsuc  8137  nominpos  10204  nnunb  10217  indstr  10545  eirr  12804  sqr2irr  12848  vdwap0  13344  zfbas  17928  aaliou3lem9  20267  vma1  20949  hatomistici  23865  wfrlem16  25553  linedegen  26077  limsucncmpi  26195  psgnunilem3  27396  elpadd0  30606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2710  df-rex 2711
  Copyright terms: Public domain W3C validator