Theorem nrexdv 2769

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 2749	. 2 |- ( ph -> A. x e. A -. ps )
3		ralnex 2676	. 2 |- ( A. x e. A -. ps <-> -. E. x e. A ps )
4	2, 3	sylib 189	1 |- ( ph -> -. E. x e. A ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 359   e. wcel 1721   A.wral 2666   E.wrex 2667

This theorem is referenced by:  class2set  4327  peano5  4827  onnseq  6565  oalimcl  6762  omlimcl  6780  oeeulem  6803  nneob  6854  wemappo  7474  setind  7629  cardlim  7815  cardaleph  7926  cflim2  8099  fin23lem38  8185  isf32lem5  8193  winainflem  8524  winalim2  8527  supmul1  9929  ixxub  10893  ixxlb  10894  rlimuni  12299  rlimcld2  12327  rlimno1  12402  harmonic  12593  eirr  12759  ruclem12  12795  dvdsle  12850  prmreclem5  13243  prmreclem6  13244  vdwnnlem3  13320  frgpnabllem1  15439  ablfacrplem  15578  lbsextlem3  16187  lmmo  17398  fbasfip  17853  hauspwpwf1  17972  alexsublem  18028  tsmsfbas  18110  iccntr  18805  reconnlem2  18811  evth  18937  bcthlem5  19234  minveclem3b  19282  itg2seq  19587  dvferm1  19822  dvferm2  19824  aaliou3lem9  20220  taylthlem2  20243  vma1  20902  pntlem3  21256  ostth2lem1  21265  ballotlemimin  24716  poseq  25467  nocvxminlem  25558  supaddc  26137  tailfb  26296  fdc  26339  heibor1lem  26408  heiborlem8  26417  cmpfiiin  26641  otiunsndisj  27954  atlatmstc  29802  pmap0  30247  hdmap14lem4a  32357

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 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672