Theorem nrexdv 2913

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

Assertion

Ref	Expression
nrexdv

Distinct variable group:   ,

Proof of Theorem nrexdv

Step	Hyp	Ref	Expression
1		nrexdv.1	. . 3
2	1	ralrimiva 2871	. 2
3		ralnex 2903	. 2
4	2, 3	sylib 196	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807  E.wrex 2808

This theorem is referenced by:  class2set  4619  otiunsndisj  4758  peano5  6723  onnseq  7034  oalimcl  7228  omlimcl  7246  oeeulem  7269  nneob  7320  wemappo  7995  setind  8186  cardlim  8374  cardaleph  8491  cflim2  8664  fin23lem38  8750  isf32lem5  8758  winainflem  9092  winalim2  9095  supmul1  10533  ixxub  11579  ixxlb  11580  supicclub2  11700  rlimuni  13373  rlimcld2  13401  rlimno1  13476  harmonic  13670  eirr  13938  ruclem12  13974  dvdsle  14031  prmreclem5  14438  prmreclem6  14439  vdwnnlem3  14515  frgpnabllem1  16877  ablfacrplem  17116  lbsextlem3  17806  lmmo  19881  fbasfip  20369  hauspwpwf1  20488  alexsublem  20544  tsmsfbas  20626  iccntr  21326  reconnlem2  21332  evth  21459  bcthlem5  21767  minveclem3b  21843  itg2seq  22149  dvferm1  22386  dvferm2  22388  aaliou3lem9  22746  taylthlem2  22769  vma1  23440  pntlem3  23794  ostth2lem1  23803  tglowdim1i  23892  2spotiundisj  25062  2spot0  25064  ordtconlem1  27906  ballotlemimin  28444  poseq  29333  nocvxminlem  29450  supaddc  30041  tailfb  30195  fdc  30238  heibor1lem  30305  heiborlem8  30314  cmpfiiin  30629  limcrecl  31635  dirkercncflem2  31886  fourierdlem20  31909  fourierdlem42  31931  fourierdlem46  31935  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  otiunsndisjX  32301  atlatmstc  35044  pmap0  35489  hdmap14lem4a  37601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813