Theorem nrexdv 2920

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 2878	. 2 |- ( ph -> A. x e. A -. ps )
3		ralnex 2910	. 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 1767   A.wral 2814   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820

This theorem is referenced by:  class2set  4614  otiunsndisj  4753  peano5  6707  onnseq  7015  oalimcl  7209  omlimcl  7227  oeeulem  7250  nneob  7301  wemappo  7974  setind  8165  cardlim  8353  cardaleph  8470  cflim2  8643  fin23lem38  8729  isf32lem5  8737  winainflem  9071  winalim2  9074  supmul1  10508  ixxub  11550  ixxlb  11551  rlimuni  13336  rlimcld2  13364  rlimno1  13439  harmonic  13633  eirr  13799  ruclem12  13835  dvdsle  13890  prmreclem5  14297  prmreclem6  14298  vdwnnlem3  14374  frgpnabllem1  16680  ablfacrplem  16918  lbsextlem3  17606  lmmo  19675  fbasfip  20132  hauspwpwf1  20251  alexsublem  20307  tsmsfbas  20389  iccntr  21089  reconnlem2  21095  evth  21222  bcthlem5  21530  minveclem3b  21606  itg2seq  21912  dvferm1  22149  dvferm2  22151  aaliou3lem9  22508  taylthlem2  22531  vma1  23196  pntlem3  23550  ostth2lem1  23559  ordtconlem1  27570  ballotlemimin  28112  poseq  28938  nocvxminlem  29055  supaddc  29646  tailfb  29826  fdc  29869  heibor1lem  29936  heiborlem8  29945  cmpfiiin  30261  dirkercncflem2  31432  fourierdlem65  31500  atlatmstc  34134  pmap0  34579  hdmap14lem4a  36689