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

Theorem ralrimdva 2875
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.)
Hypothesis
Ref Expression
ralrimdva.1
Assertion
Ref Expression
ralrimdva
Distinct variable groups:   ,   ,

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4
21expimpd 603 . . 3
32expcomd 438 . 2
43ralrimdv 2873 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralxfrd  4666  isoselem  6237  resixpfo  7527  findcard  7779  ordtypelem2  7965  alephinit  8497  isfin2-2  8720  axpre-sup  9567  nnsub  10599  ublbneg  11195  xralrple  11433  supxrunb1  11540  expnlbnd2  12297  faclbnd4lem4  12374  hashbc  12502  cau3lem  13187  limsupbnd2  13306  climrlim2  13370  climshftlem  13397  subcn2  13417  isercoll  13490  climsup  13492  serf0  13503  iseralt  13507  incexclem  13648  sqrt2irr  13982  pclem  14362  prmpwdvds  14422  vdwlem10  14508  vdwlem13  14511  ramtlecl  14518  ramub  14531  ramcl  14547  iscatd  15070  clatleglb  15756  mrcmndind  15997  grpinveu  16084  issubg4  16220  gexdvds  16604  sylow2alem2  16638  obselocv  18759  scmatscm  19015  tgcn  19753  tgcnp  19754  lmconst  19762  cncls2  19774  cncls  19775  cnntr  19776  lmss  19799  cnt0  19847  isnrm2  19859  isreg2  19878  cmpsublem  19899  cmpsub  19900  tgcmp  19901  islly2  19985  kgencn2  20058  txdis  20133  txlm  20149  kqt0lem  20237  isr0  20238  regr1lem2  20241  cmphaushmeo  20301  cfinufil  20429  ufilen  20431  flimopn  20476  fbflim2  20478  fclsnei  20520  fclsbas  20522  fclsrest  20525  flimfnfcls  20529  fclscmp  20531  ufilcmp  20533  isfcf  20535  fcfnei  20536  cnpfcf  20542  tsmsresOLD  20645  tsmsres  20646  tsmsxp  20657  blbas  20933  prdsbl  20994  metss  21011  metcnp3  21043  bndth  21458  lebnumii  21466  iscfil3  21712  iscmet3lem1  21730  equivcfil  21738  equivcau  21739  ellimc3  22283  lhop1  22415  dvfsumrlim  22432  ftc1lem6  22442  fta1g  22568  dgrco  22672  plydivex  22693  fta1  22704  vieta1  22708  ulmshftlem  22784  ulmcaulem  22789  mtest  22799  cxpcn3lem  23121  cxploglim  23307  ftalem3  23348  dchrisumlem3  23676  pntibnd  23778  ostth2lem2  23819  grpoinveu  25224  isgrp2d  25237  nmcvcn  25605  blocnilem  25719  ubthlem3  25788  htthlem  25834  spansni  26475  bra11  27027  lmxrge0  27934  mrsubff1  28874  msubff1  28916  fin2so  30040  ftc1cnnc  30089  fnemeet2  30185  fnejoin2  30187  incsequz2  30242  geomcau  30252  caushft  30254  sstotbnd2  30270  isbnd2  30279  totbndbnd  30285  ismtybndlem  30302  heibor  30317  climinf  31612  ralbinrald  32204  ralxfrd2  32303  snlindsntorlem  33071  atlatle  35045  cvlcvr1  35064  ltrnid  35859  ltrneq2  35872
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-ral 2812
  Copyright terms: Public domain W3C validator