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

Theorem rexlimdvaa 2950
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypothesis
Ref Expression
rexlimdvaa.1
Assertion
Ref Expression
rexlimdvaa
Distinct variable groups:   ,   ,

Proof of Theorem rexlimdvaa
StepHypRef Expression
1 rexlimdvaa.1 . . 3
21expr 615 . 2
32rexlimdva 2949 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexlimddv  2953  tz7.7  4909  isofrlem  6236  nnawordex  7305  oaabs2  7313  fiin  7902  marypha1lem  7913  wemaplem3  7994  cantnflt  8112  cantnfltOLD  8142  fseqenlem2  8427  cardaleph  8491  coftr  8674  fin23lem26  8726  fin1a2lem13  8813  fpwwe2  9042  r1wunlim  9136  wunex2  9137  inttsk  9173  grur1  9219  inaprc  9235  receu  10219  zsupss  11200  xralrple  11433  rexanuz  13178  limsupval2  13303  caucvgb  13502  fsumiun  13635  rpnnen2  13959  dvdsval2  13989  prmind2  14228  pcprmpw2  14405  pockthg  14424  prmreclem5  14438  vdwlem6  14504  vdwlem10  14508  sscpwex  15184  drsdirfi  15567  psgnunilem3  16521  sylow3lem2  16648  efgsfo  16757  lt6abl  16897  ghmcyg  16898  unitgrp  17316  irredrmul  17356  drngnidl  17877  znunit  18602  tgcl  19471  neiint  19605  restopnb  19676  ordtrest2lem  19704  pnfnei  19721  mnfnei  19722  iscnp4  19764  haust1  19853  ordthauslem  19884  tgcmp  19901  t1conperf  19937  2ndc1stc  19952  2ndcdisj  19957  islly2  19985  nllyrest  19987  reftr  20015  comppfsc  20033  ptbasfi  20082  ptcnp  20123  xkococnlem  20160  tgqtop  20213  fbssfi  20338  fgabs  20380  neifil  20381  trfil2  20388  elfm2  20449  elfm3  20451  rnelfmlem  20453  fmfnfmlem4  20458  flffbas  20496  fclsfnflim  20528  ptcmplem4  20555  tsmsxp  20657  blssexps  20929  blssex  20930  icccmplem3  21329  cnheibor  21455  pi1blem  21539  iscfil3  21712  iscmet3lem2  21731  cmetss  21753  ovolicc2  21933  nulmbl2  21947  volsup  21966  dyadmbllem  22008  itg2const2  22148  bddmulibl  22245  limcflf  22285  itgsubst  22450  ulmdvlem3  22797  xrlimcnp  23298  amgm  23320  dchrptlem2  23540  lgsne0  23608  lgsqr  23621  lgsquadlem1  23629  dchrvmasumif  23688  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem3  23704  dchrisum0  23705  dchrmusum  23709  dchrvmasum  23710  chpdifbnd  23740  pntrlog2bnd  23769  pntibndlem3  23777  pntibnd  23778  pntleml  23796  ostth  23824  brbtwn2  24208  colinearalg  24213  cusgrafilem1  24479  nmobndi  25690  spansneleq  26488  ofrn2  27480  xreceu  27618  ordtrest2NEWlem  27904  dya2iocnei  28253  conpcon  28680  cvmsss2  28719  cvmlift2lem10  28757  cvmlift3lem2  28765  nodenselem5  29445  nobndlem6  29457  outsidele  29782  mblfinlem1  30051  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  cnambfre  30063  itg2addnclem  30066  itg2addnclem3  30068  bddiblnc  30085  ftc1anclem7  30096  ftc1anc  30098  neibastop1  30177  neibastop2lem  30178  fdc  30238  sstotbnd2  30270  sstotbnd  30271  isbndx  30278  ssbnd  30284  totbndbnd  30285  heibor  30317  unichnidl  30428  elrfi  30626  fnwe2lem2  30997  hbtlem5  31077  2zrngamgm  32745  pexmidlem8N  35701
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