Theorem nrexdv 3001

Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.)

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  class2set  4832  otiunsndisj  4980  peano5  7089  onnseq  7441  oalimcl  7640  omlimcl  7658  oeeulem  7681  nneob  7732  wemappo  8454  setind  8610  cardlim  8798  cardaleph  8912  cflim2  9085  fin23lem38  9171  isf32lem5  9179  winainflem  9515  winalim2  9518  supaddc  10990  supmul1  10992  ixxub  12196  ixxlb  12197  supicclub2  12323  s3iunsndisj  13707  rlimuni  14281  rlimcld2  14309  rlimno1  14384  harmonic  14591  eirr  14933  ruclem12  14970  dvdsle  15032  prmreclem5  15624  prmreclem6  15625  vdwnnlem3  15701  frgpnabllem1  18276  ablfacrplem  18464  lbsextlem3  19160  lmmo  21184  fbasfip  21672  hauspwpwf1  21791  alexsublem  21848  tsmsfbas  21931  iccntr  22624  reconnlem2  22630  evth  22758  bcthlem5  23125  minveclem3b  23199  itg2seq  23509  dvferm1  23748  dvferm2  23750  aaliou3lem9  24105  taylthlem2  24128  vma1  24892  pntlem3  25298  ostth2lem1  25307  tglowdim1i  25396  ordtconnlem1  29970  ballotlemimin  30567  poseq  31750  nosupbnd1lem4  31857  nocvxminlem  31893  tailfb  32372  fdc  33541  heibor1lem  33608  heiborlem8  33617  atlatmstc  34606  pmap0  35051  hdmap14lem4a  37163  cmpfiiin  37260  limcrecl  39861  dirkercncflem2  40321  fourierdlem20  40344  fourierdlem42  40366  fourierdlem46  40369  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  otiunsndisjX  41298