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

Theorem nrex 2841
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 2766 . 2  |-  A. x  e.  A  -.  ps
3 ralnex 2834 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3mpbi 213 1  |-  -.  E. x  e.  A  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1904   A.wral 2756   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-ral 2761  df-rex 2762
This theorem is referenced by:  rex0  3737  iun0  4325  canth  6267  orduninsuc  6689  wfrlem16  7069  wofib  8078  cfsuc  8705  nominpos  10872  nnunb  10889  indstr  11250  eirr  14334  sqrt2irr  14378  vdwap0  15005  psgnunilem3  17215  bwth  20502  zfbas  20989  aaliou3lem9  23385  vma1  24172  hatomistici  28096  esumrnmpt2  28963  linedegen  30981  limsucncmpi  31176  elpadd0  33445  fourierdlem62  38144  etransc  38261  0nodd  40318  2nodd  40320  1neven  40440
  Copyright terms: Public domain W3C validator