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

Theorem nrexdv 2809
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 2789 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2715 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3sylib 196 1  |-  ( ph  ->  -.  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1755   A.wral 2705   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  class2set  4447  peano5  6488  onnseq  6791  oalimcl  6987  omlimcl  7005  oeeulem  7028  nneob  7079  wemappo  7751  setind  7942  cardlim  8130  cardaleph  8247  cflim2  8420  fin23lem38  8506  isf32lem5  8514  winainflem  8847  winalim2  8850  supmul1  10282  ixxub  11308  ixxlb  11309  rlimuni  13011  rlimcld2  13039  rlimno1  13114  harmonic  13303  eirr  13469  ruclem12  13505  dvdsle  13560  prmreclem5  13963  prmreclem6  13964  vdwnnlem3  14040  frgpnabllem1  16330  ablfacrplem  16539  lbsextlem3  17162  lmmo  18825  fbasfip  19282  hauspwpwf1  19401  alexsublem  19457  tsmsfbas  19539  iccntr  20239  reconnlem2  20245  evth  20372  bcthlem5  20680  minveclem3b  20756  itg2seq  21061  dvferm1  21298  dvferm2  21300  aaliou3lem9  21700  taylthlem2  21723  vma1  22388  pntlem3  22742  ostth2lem1  22751  ordtconlem1  26207  ballotlemimin  26735  poseq  27560  nocvxminlem  27677  supaddc  28258  tailfb  28439  fdc  28482  heibor1lem  28549  heiborlem8  28558  cmpfiiin  28875  otiunsndisj  29975  atlatmstc  32534  pmap0  32979  hdmap14lem4a  35089
  Copyright terms: Public domain W3C validator