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

Theorem rexlimdv 2947
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Hypothesis
Ref Expression
rexlimdv.1
Assertion
Ref Expression
rexlimdv
Distinct variable groups:   ,   ,

Proof of Theorem rexlimdv
StepHypRef Expression
1 rexlimdv.1 . . . 4
21com3l 81 . . 3
32rexlimiv 2943 . 2
43com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexlimdva  2949  rexlimdv3a  2951  rexlimdvw  2952  rexlimdvv  2955  elpwunsn  4070  trintss  4561  eldmrexrnb  6038  dffo3  6046  weniso  6250  ssorduni  6621  onint  6630  limuni3  6687  funcnvuni  6753  frxp  6910  smoiun  7051  tfrlem9  7073  oaordex  7226  oalimcl  7228  oaass  7229  omlimcl  7246  fisucdomOLD  7743  findcard3  7783  frfi  7785  unblem1  7792  ordiso2  7961  inf3lem3  8068  noinfepOLD  8098  r1sdom  8213  tz9.12lem3  8228  karden  8334  infxpenlem  8412  cardinfima  8499  iunfictbso  8516  dfac5  8530  cfflb  8660  cfcoflem  8673  cfcof  8675  fin23lem11  8718  fin23lem30  8743  fin1a2lem13  8813  axdc3lem2  8852  konigthlem  8964  alephval2  8968  pwcfsdom  8979  fpwwe2lem12  9040  tskuni  9182  axgroth6  9227  nqereu  9328  genpnmax  9406  ltaddpr  9433  recexsrlem  9501  mulgt0sr  9503  recexsr  9505  axrrecex  9561  axpre-sup  9567  addid1  9781  addid2  9784  recex  10206  zdiv  10958  btwnz  10991  lbzbi  11199  qbtwnre  11427  caubnd  13191  divalglem9  14059  unbenlem  14426  firest  14830  imasmnd2  15957  imasgrp2  16185  pmtrfrn  16483  pgpfi  16625  sylow2blem3  16642  imasring  17268  lspsneq  17768  lspdisj  17771  unitgOLD  19469  fctop  19505  cctop  19507  elcls  19574  elcls3  19584  subbascn  19755  cmpsublem  19899  cmpsub  19900  nllyidm  19990  comppfsc  20033  ptpjopn  20113  fbfinnfr  20342  filin  20355  isfil2  20357  infil  20364  fgss2  20375  fgfil  20376  fgcl  20379  fgabs  20380  elfm2  20449  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmco  20462  flffbas  20496  cnpflf2  20501  fclscf  20526  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  neibl  21004  met2ndc  21026  metcnp3  21043  icccmplem2  21328  xrge0tsms  21339  fgcfil  21710  volfiniun  21957  dyadmax  22007  dyadmbllem  22008  c1liplem1  22397  dgrlem  22626  axcontlem10  24276  usgrarnedg  24384  erclwwlksym  24814  erclwwlknsym  24826  lpni  25181  grpoidinvlem3  25208  grporcan  25223  grpoinvf  25242  nmosetre  25679  omlsii  26321  spansncol  26486  spansnss  26489  normcan  26494  spanunsni  26497  h1datomi  26499  nmopsetretALT  26782  nmfnsetre  26796  branmfn  27024  superpos  27273  chjatom  27276  cvbr4i  27286  atomli  27301  xrge0tsmsd  27775  eulerpartlemgh  28317  dfon2lem6  29220  trpredrec  29321  colineardim1  29711  finminlem  30136  nn0prpwlem  30140  neibastop2lem  30178  neibastop2  30179  fgmin  30188  heiborlem10  30316  prtlem15  30616  isnacs3  30642  jm2.26  30944  fnwe2lem2  30997  hbtlem5  31077  islptre  31625  limcperiod  31634  limclner  31657  coskpi2  31666  cosknegpi  31669  icccncfext  31690  stoweidlem27  31809  stoweidlem59  31841  fourierdlem41  31930  fourierdlem42  31931  fourierdlem70  31959  fourierdlem71  31960  fourierdlem81  31970  fourierswlem  32013  islindeps2  33084  lshpcmp  34713  lsatn0  34724  lsatcmp  34728  lsmsat  34733  lsatcv0  34756  l1cvpat  34779  eqlkr  34824  lshpkrlem1  34835  lshpkrlem6  34840  lfl1dim  34846  lfl1dim2N  34847  lkrss2N  34894  athgt  35180  3dim2  35192  llnle  35242  llncmp  35246  lplnle  35264  lplnnle2at  35265  llncvrlpln2  35281  llncvrlpln  35282  lplncmp  35286  lplnexllnN  35288  lvolnle3at  35306  lplncvrlvol2  35339  lplncvrlvol  35340  lvolcmp  35341  pointpsubN  35475  pclfinN  35624  pclfinclN  35674  osumcllem11N  35690  pexmidlem4N  35697  cdleme17d3  36222  cdlemeg46gfre  36258  cdleme48gfv1  36262  cdleme50trn2  36277  trlord  36295  cdlemg6e  36348  cdlemj3  36549  diaelrnN  36772  diaintclN  36785  dia2dimlem6  36796  cdlemm10N  36845  dibintclN  36894  dihord6apre  36983  dihord5b  36986  dihord5apre  36989  dihglblem5apreN  37018  dihglblem2N  37021  dihglblem3N  37022  dihglbcpreN  37027  dihintcl  37071  lclkrlem2y  37258  lcfrvalsnN  37268
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