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

Theorem nrexdv 2646
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 2626 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2553 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3sylib 188 1  |-  ( ph  ->  -.  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  class2set  4178  peano5  4679  onnseq  6361  oalimcl  6558  omlimcl  6576  oeeulem  6599  nneob  6650  wemappo  7264  setind  7419  cardlim  7605  cardaleph  7716  cflim2  7889  fin23lem38  7975  isf32lem5  7983  winainflem  8315  winalim2  8318  supmul1  9719  ixxub  10677  ixxlb  10678  rlimuni  12024  rlimcld2  12052  rlimno1  12127  harmonic  12317  eirr  12483  ruclem12  12519  dvdsle  12574  prmreclem5  12967  prmreclem6  12968  vdwnnlem3  13044  frgpnabllem1  15161  ablfacrplem  15300  lbsextlem3  15913  lmmo  17108  fbasfip  17563  hauspwpwf1  17682  alexsublem  17738  tsmsfbas  17810  iccntr  18326  reconnlem2  18332  evth  18457  bcthlem5  18750  minveclem3b  18792  itg2seq  19097  dvferm1  19332  dvferm2  19334  aaliou3lem9  19730  taylthlem2  19753  vma1  20404  pntlem3  20758  ostth2lem1  20767  poseq  24253  nocvxminlem  24344  tailfb  26326  fdc  26455  heibor1lem  26533  heiborlem8  26542  cmpfiiin  26772  atlatmstc  29509  pmap0  29954  hdmap14lem4a  32064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator