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

Theorem nrexdv 2752
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 2732 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2659 . 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 1717   A.wral 2649   E.wrex 2650
This theorem is referenced by:  class2set  4308  peano5  4808  onnseq  6542  oalimcl  6739  omlimcl  6757  oeeulem  6780  nneob  6831  wemappo  7451  setind  7606  cardlim  7792  cardaleph  7903  cflim2  8076  fin23lem38  8162  isf32lem5  8170  winainflem  8501  winalim2  8504  supmul1  9905  ixxub  10869  ixxlb  10870  rlimuni  12271  rlimcld2  12299  rlimno1  12374  harmonic  12565  eirr  12731  ruclem12  12767  dvdsle  12822  prmreclem5  13215  prmreclem6  13216  vdwnnlem3  13292  frgpnabllem1  15411  ablfacrplem  15550  lbsextlem3  16159  lmmo  17366  fbasfip  17821  hauspwpwf1  17940  alexsublem  17996  tsmsfbas  18078  iccntr  18723  reconnlem2  18729  evth  18855  bcthlem5  19150  minveclem3b  19196  itg2seq  19501  dvferm1  19736  dvferm2  19738  aaliou3lem9  20134  taylthlem2  20157  vma1  20816  pntlem3  21170  ostth2lem1  21179  ballotlemimin  24542  poseq  25277  nocvxminlem  25368  supaddc  25947  tailfb  26097  fdc  26140  heibor1lem  26209  heiborlem8  26218  cmpfiiin  26442  atlatmstc  29434  pmap0  29879  hdmap14lem4a  31989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator