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

Theorem nrexdv 2659
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 2639 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2566 . 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 1696   A.wral 2556   E.wrex 2557
This theorem is referenced by:  class2set  4194  peano5  4695  onnseq  6377  oalimcl  6574  omlimcl  6592  oeeulem  6615  nneob  6666  wemappo  7280  setind  7435  cardlim  7621  cardaleph  7732  cflim2  7905  fin23lem38  7991  isf32lem5  7999  winainflem  8331  winalim2  8334  supmul1  9735  ixxub  10693  ixxlb  10694  rlimuni  12040  rlimcld2  12068  rlimno1  12143  harmonic  12333  eirr  12499  ruclem12  12535  dvdsle  12590  prmreclem5  12983  prmreclem6  12984  vdwnnlem3  13060  frgpnabllem1  15177  ablfacrplem  15316  lbsextlem3  15929  lmmo  17124  fbasfip  17579  hauspwpwf1  17698  alexsublem  17754  tsmsfbas  17826  iccntr  18342  reconnlem2  18348  evth  18473  bcthlem5  18766  minveclem3b  18808  itg2seq  19113  dvferm1  19348  dvferm2  19350  aaliou3lem9  19746  taylthlem2  19769  vma1  20420  pntlem3  20774  ostth2lem1  20783  poseq  24324  nocvxminlem  24415  supaddc  24995  tailfb  26429  fdc  26558  heibor1lem  26636  heiborlem8  26645  cmpfiiin  26875  atlatmstc  30131  pmap0  30576  hdmap14lem4a  32686
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator