Theorem nrexdv 2842

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 376   e. wcel 1904   A.wral 2756   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-ral 2761  df-rex 2762

This theorem is referenced by:  class2set  4568  otiunsndisj  4707  peano5  6735  onnseq  7081  oalimcl  7279  omlimcl  7297  oeeulem  7320  nneob  7371  wemappo  8082  setind  8236  cardlim  8424  cardaleph  8538  cflim2  8711  fin23lem38  8797  isf32lem5  8805  winainflem  9136  winalim2  9139  supaddc  10596  supmul1  10598  ixxub  11681  ixxlb  11682  ixxlbOLD  11683  supicclub2  11809  rlimuni  13691  rlimcld2  13719  rlimno1  13794  harmonic  13994  eirr  14334  ruclem12  14370  dvdsle  14427  prmreclem5  14943  prmreclem6  14944  vdwnnlem3  15026  frgpnabllem1  17587  ablfacrplem  17776  lbsextlem3  18461  lmmo  20473  fbasfip  20961  hauspwpwf1  21080  alexsublem  21137  tsmsfbas  21220  iccntr  21917  reconnlem2  21923  evth  22065  bcthlem5  22374  minveclem3b  22448  minveclem3bOLD  22460  itg2seq  22779  dvferm1  23016  dvferm2  23018  aaliou3lem9  23385  taylthlem2  23408  vma1  24172  pntlem3  24526  ostth2lem1  24535  tglowdim1i  24624  2spotiundisj  25869  2spot0  25871  ordtconlem1  28804  ballotlemimin  29411  ballotlemiminOLD  29449  poseq  30562  nocvxminlem  30650  tailfb  31104  fdc  32138  heibor1lem  32205  heiborlem8  32214  atlatmstc  32956  pmap0  33401  hdmap14lem4a  35513  cmpfiiin  35610  limcrecl  37806  dirkercncflem2  38078  fourierdlem20  38101  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem46  38128  fourierdlem63  38145  fourierdlem64  38146  fourierdlem65  38147  otiunsndisjX  39152