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

Theorem nrexdv 2801
Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
Hypothesis
Ref Expression
nrexdv.1  |-  ( (
ph  /\  x  e.  A )  ->  -.  ps )
Assertion
Ref Expression
nrexdv  |-  ( ph  ->  -.  E. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem nrexdv
StepHypRef Expression
1 nrexdv.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  -.  ps )
21ralrimiva 2781 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2707 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3sylib 189 1  |-  ( ph  ->  -.  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2697   E.wrex 2698
This theorem is referenced by:  class2set  4359  peano5  4860  onnseq  6598  oalimcl  6795  omlimcl  6813  oeeulem  6836  nneob  6887  wemappo  7508  setind  7663  cardlim  7849  cardaleph  7960  cflim2  8133  fin23lem38  8219  isf32lem5  8227  winainflem  8558  winalim2  8561  supmul1  9963  ixxub  10927  ixxlb  10928  rlimuni  12334  rlimcld2  12362  rlimno1  12437  harmonic  12628  eirr  12794  ruclem12  12830  dvdsle  12885  prmreclem5  13278  prmreclem6  13279  vdwnnlem3  13355  frgpnabllem1  15474  ablfacrplem  15613  lbsextlem3  16222  lmmo  17434  fbasfip  17890  hauspwpwf1  18009  alexsublem  18065  tsmsfbas  18147  iccntr  18842  reconnlem2  18848  evth  18974  bcthlem5  19271  minveclem3b  19319  itg2seq  19624  dvferm1  19859  dvferm2  19861  aaliou3lem9  20257  taylthlem2  20280  vma1  20939  pntlem3  21293  ostth2lem1  21302  ballotlemimin  24753  poseq  25513  nocvxminlem  25610  supaddc  26201  tailfb  26360  fdc  26403  heibor1lem  26472  heiborlem8  26481  cmpfiiin  26705  otiunsndisj  28020  atlatmstc  30018  pmap0  30463  hdmap14lem4a  32573
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator