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

Step	Hyp	Ref	Expression
1		nrexdv.1	. . 3 |- ( ( ph /\ x e. A ) -> -. ps )
2	1	ralrimiva 2789	. 2 |- ( ph -> A. x e. A -. ps )
3		ralnex 2715	. 2 |- ( A. x e. A -. ps <-> -. E. x e. A ps )
4	2, 3	sylib 196	1 |- ( ph -> -. E. x e. A ps )

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