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

Theorem nrex 2918
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 2893 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2848 . 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 1758   A.wral 2796   E.wrex 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-ral 2801  df-rex 2802
This theorem is referenced by:  rex0  3754  iun0  4329  canth  6153  orduninsuc  6559  wofib  7865  cfsuc  8532  nominpos  10667  nnunb  10681  indstr  11029  eirr  13600  sqr2irr  13644  vdwap0  14150  psgnunilem3  16116  bwth  19140  zfbas  19596  aaliou3lem9  21944  vma1  22632  hatomistici  25913  wfrlem16  27878  linedegen  28313  limsucncmpi  28430  elpadd0  33772
  Copyright terms: Public domain W3C validator