Theorem nrexdv 2840

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 2820	. 2 |- ( ph -> A. x e. A -. ps )
3		ralnex 2746	. 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 1756   A.wral 2736   E.wrex 2737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742

This theorem is referenced by:  class2set  4480  peano5  6520  onnseq  6826  oalimcl  7020  omlimcl  7038  oeeulem  7061  nneob  7112  wemappo  7784  setind  7975  cardlim  8163  cardaleph  8280  cflim2  8453  fin23lem38  8539  isf32lem5  8547  winainflem  8881  winalim2  8884  supmul1  10316  ixxub  11342  ixxlb  11343  rlimuni  13049  rlimcld2  13077  rlimno1  13152  harmonic  13342  eirr  13508  ruclem12  13544  dvdsle  13599  prmreclem5  14002  prmreclem6  14003  vdwnnlem3  14079  frgpnabllem1  16372  ablfacrplem  16588  lbsextlem3  17263  lmmo  19006  fbasfip  19463  hauspwpwf1  19582  alexsublem  19638  tsmsfbas  19720  iccntr  20420  reconnlem2  20426  evth  20553  bcthlem5  20861  minveclem3b  20937  itg2seq  21242  dvferm1  21479  dvferm2  21481  aaliou3lem9  21838  taylthlem2  21861  vma1  22526  pntlem3  22880  ostth2lem1  22889  ordtconlem1  26376  ballotlemimin  26910  poseq  27736  nocvxminlem  27853  supaddc  28443  tailfb  28624  fdc  28667  heibor1lem  28734  heiborlem8  28743  cmpfiiin  29059  otiunsndisj  30158  atlatmstc  33060  pmap0  33505  hdmap14lem4a  35615