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

Theorem nrexdv 2811
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 2791 . 2  |-  ( ph  ->  A. x  e.  A  -.  ps )
3 ralnex 2717 . 2  |-  ( A. x  e.  A  -.  ps 
<->  -.  E. x  e.  A  ps )
42, 3sylib 190 1  |-  ( ph  ->  -.  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360    e. wcel 1726   A.wral 2707   E.wrex 2708
This theorem is referenced by:  class2set  4370  peano5  4871  onnseq  6609  oalimcl  6806  omlimcl  6824  oeeulem  6847  nneob  6898  wemappo  7521  setind  7676  cardlim  7864  cardaleph  7975  cflim2  8148  fin23lem38  8234  isf32lem5  8242  winainflem  8573  winalim2  8576  supmul1  9978  ixxub  10942  ixxlb  10943  rlimuni  12349  rlimcld2  12377  rlimno1  12452  harmonic  12643  eirr  12809  ruclem12  12845  dvdsle  12900  prmreclem5  13293  prmreclem6  13294  vdwnnlem3  13370  frgpnabllem1  15489  ablfacrplem  15628  lbsextlem3  16237  lmmo  17449  fbasfip  17905  hauspwpwf1  18024  alexsublem  18080  tsmsfbas  18162  iccntr  18857  reconnlem2  18863  evth  18989  bcthlem5  19286  minveclem3b  19334  itg2seq  19637  dvferm1  19874  dvferm2  19876  aaliou3lem9  20272  taylthlem2  20295  vma1  20954  pntlem3  21308  ostth2lem1  21317  ballotlemimin  24768  poseq  25533  nocvxminlem  25650  supaddc  26245  tailfb  26420  fdc  26463  heibor1lem  26532  heiborlem8  26541  cmpfiiin  26765  otiunsndisj  28081  atlatmstc  30191  pmap0  30636  hdmap14lem4a  32746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator