Theorem rexlimdv3a 2951

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2947. (Contributed by NM, 7-Jun-2015.)

Hypothesis

Ref	Expression
rexlimdv3a.1

Assertion

Ref	Expression
rexlimdv3a

Distinct variable groups:   ,   ,

Proof of Theorem rexlimdv3a

Step	Hyp	Ref	Expression
1		rexlimdv3a.1	. . 3
2	1	3exp 1195	. 2
3	2	rexlimdv 2947	1

Syntax hints:  ->wi 4  /\w3a 973  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  sorpssuni  6589  sorpssint  6590  tcrank  8323  rpnnen1lem5  11241  hashfun  12495  resqrex  13084  resqrtcl  13087  lbsextlem3  17806  cmpsublem  19899  cmpcld  19902  ovoliunlem2  21914  isblo3i  25716  trisegint  29678  itg2addnclem  30066  areacirclem2  30108  rpnnen3lem  30973  dvconstbi  31239  expgrowth  31240  limccog  31626  0ellimcdiv  31655  cosknegpi  31669  cncfshift  31676  cncfperiod  31681  cncfuni  31689  icccncfext  31690  dvbdfbdioolem1  31725  itgperiod  31780  stoweidlem57  31839  fourierdlem12  31901  fourierdlem48  31937  fourierdlem49  31938  fourierdlem52  31941  fourierdlem54  31943  fourierdlem68  31957  fourierdlem77  31966  fourierdlem83  31972  fourierdlem87  31976  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  fourierdlem114  32003  etransclem24  32041  etransclem32  32049  etransclem48  32065  sigarcol  32081  lshpnelb  34709  lsatfixedN  34734  lsmsatcv  34735  lssatomic  34736  lcv1  34766  lsatcvatlem  34774  islshpcv  34778  lfl1  34795  lshpsmreu  34834  lshpkrex  34843  lshpset2N  34844  lkrlspeqN  34896  cvrval3  35137  1cvratlt  35198  ps-2b  35206  llnnleat  35237  lvolex3N  35262  lplncvrlvol2  35339  osumcllem7N  35686  lhp0lt  35727  lhpj1  35746  4atexlemex6  35798  4atexlem7  35799  trlnidat  35898  cdlemd9  35931  cdleme21h  36060  cdlemg7fvbwN  36333  cdlemg7aN  36351  cdlemg34  36438  cdlemg36  36440  cdlemg44  36459  cdlemg48  36463  tendo1ne0  36554  cdlemk26-3  36632  cdlemk55b  36686  cdleml4N  36705  dih1dimatlem0  37055  dihglblem6  37067  dochshpncl  37111  dvh4dimlem  37170  dvh3dim2  37175  dvh3dim3N  37176  dochsatshpb  37179  dochexmidlem4  37190  dochexmidlem5  37191  dochexmidlem8  37194  dochkr1  37205  dochkr1OLDN  37206  lcfl7lem  37226  lcfl6  37227  lcfl8  37229  lcfrlem16  37285  lcfrlem40  37309  mapdval2N  37357  mapdrvallem2  37372  mapdpglem24  37431  mapdh6iN  37471  mapdh8ad  37506  mapdh8e  37511  hdmap1l6i  37546  hdmapval0  37563  hdmapevec  37565  hdmapval3N  37568  hdmap10lem  37569  hdmap11lem2  37572  hdmaprnlem15N  37591  hdmaprnlem16N  37592  hdmap14lem10  37607  hdmap14lem11  37608  hdmap14lem12  37609  hdmap14lem14  37611  hgmapval0  37622  hgmapval1  37623  hgmapadd  37624  hgmapmul  37625  hgmaprnlem3N  37628  hgmaprnlem4N  37629  hgmap11  37632  hgmapvvlem3  37655

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-3an 975  df-ex 1613  df-ral 2812  df-rex 2813