Theorem nrexdv 2888

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370   e. wcel 1870   A.wral 2782   E.wrex 2783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788

This theorem is referenced by:  class2set  4592  otiunsndisj  4727  peano5  6730  onnseq  7071  oalimcl  7269  omlimcl  7287  oeeulem  7310  nneob  7361  wemappo  8064  setind  8217  cardlim  8405  cardaleph  8518  cflim2  8691  fin23lem38  8777  isf32lem5  8785  winainflem  9117  winalim2  9120  supaddc  10574  supmul1  10576  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  supicclub2  11781  rlimuni  13592  rlimcld2  13620  rlimno1  13695  harmonic  13895  eirr  14235  ruclem12  14271  dvdsle  14328  prmreclem5  14827  prmreclem6  14828  vdwnnlem3  14910  frgpnabllem1  17444  ablfacrplem  17633  lbsextlem3  18318  lmmo  20327  fbasfip  20814  hauspwpwf1  20933  alexsublem  20990  tsmsfbas  21073  iccntr  21750  reconnlem2  21756  evth  21883  bcthlem5  22189  minveclem3b  22263  itg2seq  22577  dvferm1  22814  dvferm2  22816  aaliou3lem9  23171  taylthlem2  23194  vma1  23956  pntlem3  24310  ostth2lem1  24319  tglowdim1i  24408  2spotiundisj  25635  2spot0  25637  ordtconlem1  28569  ballotlemimin  29164  poseq  30278  nocvxminlem  30364  tailfb  30818  fdc  31778  heibor1lem  31845  heiborlem8  31854  atlatmstc  32594  pmap0  33039  hdmap14lem4a  35151  cmpfiiin  35248  limcrecl  37281  dirkercncflem2  37535  fourierdlem20  37558  fourierdlem42  37580  fourierdlem46  37584  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  otiunsndisjX  38378