Theorem rexralbidv 2976

Description: Formula-building rule for restricted quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1

Assertion

Ref	Expression
rexralbidv

Distinct variable groups:   ,   ,

Proof of Theorem rexralbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3
2	1	ralbidv 2896	. 2
3	2	rexbidv 2968	1

Syntax hints:  ->wi 4  <->wb 184  A.wral 2807  E.wrex 2808

This theorem is referenced by:  freq1  4854  rexfiuz  13180  cau3lem  13187  caubnd2  13190  climi  13333  rlimi  13336  o1lo1  13360  2clim  13395  lo1le  13474  caucvgrlem  13495  caurcvgr  13496  caucvgb  13502  vdwlem10  14508  vdwlem13  14511  pmatcollpw2lem  19278  neiptopnei  19633  lmcvg  19763  lmss  19799  elpt  20073  elptr  20074  txlm  20149  tsmsi  20632  ustuqtop4  20747  isucn  20781  isucn2  20782  ucnima  20784  metcnpi  21047  metcnpi2  21048  metucnOLD  21091  metucn  21092  xrge0tsms  21339  elcncf  21393  cncfi  21398  lmmcvg  21700  lhop1  22415  ulmval  22775  ulmi  22781  ulmcaulem  22789  ulmdvlem3  22797  pntibnd  23778  pntlem3  23794  pntleml  23796  axtgcont1  23865  perpln1  24087  perpln2  24088  isperp  24089  brbtwn  24202  isgrpo  25198  ubthlem3  25788  ubth  25789  hcau  26101  hcaucvg  26103  hlimi  26105  hlimconvi  26108  hlim2  26109  elcnop  26776  elcnfn  26801  cnopc  26832  cnfnc  26849  lnopcon  26954  lnfncon  26975  riesz1  26984  xrge0tsmsd  27775  signsply0  28508  limcleqr  31650  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  cncfperiod  31681  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  fourierdlem68  31957  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  etransclem48  32065

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