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

Theorem r19.21bi 2826
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2020.)
Hypothesis
Ref Expression
r19.21bi.1
Assertion
Ref Expression
r19.21bi

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . 3
2 rsp 2823 . . 3
31, 2syl 16 . 2
43imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807
This theorem is referenced by:  r19.21be  2828  rspec2  2829  rspec3  2830  reusv6OLD  4663  ralxfr2d  4668  f1oresrab  6063  isoselem  6237  boxcutc  7532  xpf1o  7699  fineqvlem  7754  indexfi  7848  dffi3  7911  suppr  7950  supiso  7954  ordtypelem9  7972  brwdom3  8029  xpwdomg  8032  ixpiunwdom  8038  infxpenc2lem1  8417  hsmexlem4  8830  gchina  9098  wunom  9119  prcdnq  9392  prnmax  9394  dedekind  9765  dedekindle  9766  monoord2  12138  seqshft  12918  limsupgre  13304  limsupbnd1  13305  limsupbnd2  13306  climmpt2  13396  rlimcld2  13401  rlimmptrcl  13430  lo1mptrcl  13444  o1mptrcl  13445  climsup  13492  fsum2dlem  13585  fsumiun  13635  fprod2dlem  13784  iserodd  14359  vdwlem1  14499  vdwlem6  14504  vdwnnlem3  14515  imasvscafn  14934  fuciso  15344  evlfcl  15491  yonedainv  15550  acsmapd  15808  prdsmndd  15953  psgnunilem5  16519  gsummpt1n0  16992  dprdspan  17074  ablfaclem2  17137  srgi  17163  srgrz  17177  srglz  17178  issrngd  17510  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbagcon  18022  psrass1lem  18029  evlslem2  18180  mpfind  18205  gsumsmonply1  18345  gsummoncoe1  18346  evl1gsummon  18401  frgpcyg  18612  frlmgsumOLD  18801  frlmgsum  18802  uvcresum  18824  cpmatmcllem  19219  neiptoptop  19632  neiptopnei  19633  ordtrest2lem  19704  cncmp  19892  1stckgenlem  20054  ptcld  20114  dfac14  20119  txcnp  20121  ptcnplem  20122  ptcnp  20123  ptcn  20128  pthaus  20139  xkococnlem  20160  xkococn  20161  cnmpt11  20164  cnmpt1t  20166  cnmpt12  20168  cnmptkp  20181  cnmptk1  20182  cnmptkk  20184  cnmptk1p  20186  cnmptk2  20187  cnmpt2k  20189  xpstopnlem1  20310  cnpflfi  20500  ptcmplem2  20553  cnextcn  20567  cnextfres  20568  cnmpt1plusg  20586  cnmpt2plusg  20587  cnmpt1vsca  20696  cnmpt2vsca  20697  ustfilxp  20715  utoptop  20737  restutop  20740  restutopopn  20741  ucncn  20788  cfilufg  20796  trcfilu  20797  psmet0  20812  psmettri2  20813  prdsxmetlem  20871  prdsbl  20994  prdsxmslem2  21032  metutopOLD  21085  psmetutop  21086  cnmpt1ds  21347  cnmpt2ds  21348  cncfmpt2ss  21419  bndth  21458  cnmpt1ip  21687  cnmpt2ip  21688  iscmet3lem2  21731  cmetcusp1OLD  21791  cmetcusp1  21792  rrxcph  21824  ovoliunlem1  21913  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovolscalem1  21924  volfiniun  21957  uniioombllem4  21995  mbfmptcl  22044  mbfeqalem  22049  mbfres2  22052  ismbf3d  22061  mbfsup  22071  mbfinf  22072  mbflim  22075  itg1ge0  22093  itg1mulc  22111  i1fposd  22114  itg1climres  22121  mbfi1fseqlem4  22125  itg2lea  22151  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2addlem  22165  itg2cnlem1  22168  itgeqa  22220  itgss3  22221  itgfsum  22233  itgabs  22241  itggt0  22248  dvmptcl  22362  dvmptco  22375  dvlipcn  22395  dvle  22408  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvmptrecl  22425  dvfsumlem2  22428  itgparts  22448  itgsubstlem  22449  itgsubst  22450  coeeulem  22621  dgrlem  22626  dgrlb  22633  coeaddlem  22646  coecj  22675  ulmss  22792  ulmdvlem2  22796  itgulm2  22804  logtayl  23041  leibpi  23273  xrlimcnp  23298  o1cxp  23304  jensen  23318  wilthlem2  23343  sqff1o  23456  fsumdvdscom  23461  fsumdvdsmul  23471  dchrmulcl  23524  dchrmulid2  23527  dchrinv  23536  dchrisumlem3  23676  dchrvmasumlem2  23683  ostth1  23818  ercgrg  23908  f1otrg  24174  f1otrge  24175  ubthlem2  25787  fmptcof2  27502  disjdsct  27521  ressprs  27643  oduprs  27644  archiabl  27742  lmodslmd  27747  sumpr  27769  txomap  27837  qtophaus  27839  locfinreflem  27843  ordtrest2NEWlem  27904  lmdvg  27935  esumcl  28043  esumeq2d  28050  esumnul  28059  hasheuni  28091  esumcvg  28092  insiga  28137  measvunilem  28183  measvunilem0  28184  measdivcstOLD  28195  cntmeas  28197  voliune  28201  volfiniune  28202  1stmbfm  28231  2ndmbfm  28232  eulerpartlems  28299  eulerpartlemsv3  28300  eulerpartlemgvv  28315  dstrvprob  28410  lgambdd  28579  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem8  28642  ptpcon  28678  rescon  28691  cvmliftmolem2  28727  cvmlift2lem11  28758  cvmliftphtlem  28762  mclsax  28929  fin2so  30040  mblfinlem2  30052  itgabsnc  30084  itggt0cn  30087  prdsbnd  30289  prdstotbnd  30290  prdsbnd2  30291  rrnequiv  30331  fnwe2lem1  30996  rfcnnnub  31411  mptex2  31445  climinf  31612  climsuse  31614  mullimc  31622  limccog  31626  mullimcf  31629  limcperiod  31634  limcleqr  31650  neglimc  31653  0ellimcdiv  31655  limclner  31657  dvdivbd  31720  ioodvbdlimc1lem1  31728  dvnprodlem2  31744  iblsplit  31765  stoweidlem5  31787  stoweidlem16  31798  stoweidlem21  31803  stoweidlem24  31806  stoweidlem25  31807  stoweidlem28  31810  stoweidlem31  31813  stoweidlem41  31823  stoweidlem42  31824  stoweidlem44  31826  stoweidlem45  31827  stoweidlem48  31830  stoweidlem51  31833  stoweidlem54  31836  stoweidlem57  31839  stoweidlem60  31842  stoweidlem62  31844  stirlinglem5  31860  dirkercncflem3  31887  fourierdlem11  31900  fourierdlem12  31901  fourierdlem14  31903  fourierdlem15  31904  fourierdlem31  31920  fourierdlem34  31923  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem54  31943  fourierdlem69  31958  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem79  31968  fourierdlem80  31969  fourierdlem81  31970  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem113  32002  etransclem32  32049  bnj93  33921  bnj518  33944  bnj1489  34112  eqlkr3  34826  dih1dimatlem  37056  imo72b2  37993
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  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812
  Copyright terms: Public domain W3C validator