MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimiva Unicode version

Theorem rexlimiva 2945
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
Hypothesis
Ref Expression
rexlimiva.1
Assertion
Ref Expression
rexlimiva
Distinct variable group:   ,

Proof of Theorem rexlimiva
StepHypRef Expression
1 rexlimiva.1 . . 3
21ex 434 . 2
32rexlimiv 2943 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexraleqim  3225  unon  6666  tfrlem16  7081  oawordeulem  7222  nneob  7320  ominf  7752  unfilem1  7804  pwfi  7835  fival  7892  elfi2  7894  fi0  7900  fiin  7902  finnum  8350  dif1card  8409  fseqenlem2  8427  dfac8alem  8431  alephfp  8510  cflim2  8664  isfin1-3  8787  fin67  8796  isfin7-2  8797  axdc3lem  8851  axdc3lem2  8852  iunfo  8935  iundom2g  8936  winainflem  9092  rankcf  9176  map2psrpr  9508  supsrlem  9509  1re  9616  00id  9776  addid1  9781  om2uzrani  12063  uzrdgfni  12069  wrdf  12553  rexanuz  13178  r19.2uz  13184  fsum2dlem  13585  fsumcom2  13589  fprod2dlem  13784  fprodcom2  13788  0dvds  14004  modprm0  14330  cshwsidrepsw  14578  psgndiflemA  18637  ppttop  19508  epttop  19510  neips  19614  lmmo  19881  2ndctop  19948  2ndcsep  19960  fbncp  20340  fgcl  20379  filuni  20386  tgioo  21301  zcld  21318  elovolm  21886  nulmbl2  21947  ellimc3  22283  limcflf  22285  pilem3  22848  perfect  23506  2vmadivsum  23726  selberg3lem2  23743  selberg4  23746  pntrsumbnd2  23752  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntpbnd  23773  pnt3  23797  axcontlem12  24278  axcont  24279  eleclclwwlkn  24833  frgrareggt1  25116  norm1exi  26168  nmcexi  26945  lnconi  26952  pjssdif1i  27094  stri  27176  hstri  27184  stcltrthi  27197  shatomici  27277  dispcmp  27862  isrnmeas  28171  dya2iocucvr  28255  sxbrsigalem1  28256  eulerpartlemt  28310  mthmblem  28940  trpredlem1  29310  elno  29406  noreson  29420  mblfinlem3  30053  ismblfin  30055  volsupnfl  30059  dvtanlem  30064  itg2addnclem  30066  itg2addnc  30069  cover2  30204  prtlem16  30610  rexzrexnn0  30737  isnumbasgrplem2  31053  dgraalem  31094  islptre  31625  stirlinglem13  31868  stirlinglem14  31869  stirling  31871  etransc  32066  2zlidl  32740  2zrngamgm  32745  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lincsumcl  33032  lincscmcl  33033  ellcoellss  33036  bnj1398  34090  bnj1498  34117  rp-isfinite5  37743
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
  Copyright terms: Public domain W3C validator