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

Theorem rexlimivv 2954
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1
Assertion
Ref Expression
rexlimivv
Distinct variable groups:   , ,   ,

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3
21rexlimdva 2949 . 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:  2reu5  3308  opelxp  5034  opiota  6859  f1o2ndf1  6908  tfrlem5  7068  xpdom2  7632  1sdom  7742  unxpdomlem3  7746  unfi  7807  elfiun  7910  xpnum  8353  kmlem9  8559  nqereu  9328  distrlem5pr  9426  mulid1  9614  1re  9616  mul02  9779  cnegex  9782  recex  10206  creur  10555  creui  10556  cju  10557  elz2  10906  zaddcl  10929  qre  11216  qaddcl  11227  qnegcl  11228  qmulcl  11229  qreccl  11231  replim  12949  prodmo  13743  xpnnenOLD  13943  odd2np1  14046  qredeu  14248  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pythagtriplem1  14340  pcz  14404  4sqlem1  14466  4sqlem2  14467  4sqlem4  14470  mul4sq  14472  pmtr3ncom  16500  efgmnvl  16732  efgrelexlema  16767  ring1ne0  17239  txuni2  20066  tx2ndc  20152  blssioo  21300  tgioo  21301  ioorf  21982  ioorinv  21985  ioorcl  21986  dyaddisj  22005  mbfid  22043  elply  22592  vmacl  23392  efvmacl  23394  vmalelog  23480  2sqlem2  23639  mul2sq  23640  2sqlem7  23645  pntibnd  23778  ostth  23824  legval  23971  usgrasscusgra  24483  el2wlksoton  24878  el2spthsoton  24879  n4cyclfrgra  25018  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  2spotmdisj  25068  friendshipgt3  25121  lpni  25181  ipasslem5  25750  ipasslem11  25755  hhssnv  26180  shscli  26235  shsleji  26288  shsidmi  26302  spansncvi  26570  superpos  27273  chirredi  27313  mdsymlem6  27327  rnmpt2ss  27515  cnre2csqima  27893  dya2icobrsiga  28247  dya2iocnrect  28252  dya2iocucvr  28255  sxbrsigalem2  28257  afsval  28551  msubco  28891  ghomgrpilem2  29026  poseq  29333  soseq  29334  nofulllem5  29466  elaltxp  29625  altxpsspw  29627  funtransport  29681  funray  29790  funline  29792  ellines  29802  linethru  29803  itg2addnc  30069  mzpcompact2lem  30684  2reu4  32195  usgvincvad  32404  usgvincvadALT  32407  isline  35463
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