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

Theorem ralrimivw 2872
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1
Assertion
Ref Expression
ralrimivw
Distinct variable group:   ,

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3
21a1d 25 . 2
32ralrimiv 2869 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807
This theorem is referenced by:  2rmorex  3304  riinrab  4406  exse  4848  dmxp  5226  mpt2eq12  6357  ovmpt3rabdm  6535  offveqb  6562  exse2  6739  xpexgALT  6793  mpt2exg  6875  uniqs  7390  boxriin  7531  fisupg  7788  supmaxlemOLD  7945  fisup2g  7947  fisupcl  7948  ordtypelem8  7971  wemapso2  8000  cantnflem1  8129  r1val1  8225  scottex  8324  dfac12k  8548  compssiso  8775  axcclem  8858  ondomon  8959  tskuni  9182  pinq  9326  supexpr  9453  dedekind  9765  supmullem2  10535  zsupss  11200  qextlt  11431  qextle  11432  xrsupsslem  11527  xrinfmsslem  11528  supxrpnf  11539  ssnn0fi  12094  recan  13169  climconst  13366  dvdsext  14037  smupvallem  14133  smumullem  14142  pc11  14403  prmreclem4  14437  vdwmc2  14497  vdwlem8  14506  vdwlem13  14511  cshwsex  14585  cshws0  14586  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  imasplusg  14914  imasmulr  14915  imasip  14918  imasaddvallem  14926  imasvscaf  14936  quslem  14940  divsfval  14944  mrcuni  15018  catideu  15072  homfeqd  15090  comfeqd  15102  2oppccomf  15120  catcoppccl  15435  lublecllem  15618  pmtrrn  16482  pmtrfrn  16483  gsummptif1n0  16993  evlseu  18185  ip2eq  18688  frlmup4  18835  pmatcollpw2lem  19278  basdif0  19454  clsval2  19551  neif  19601  ordtbaslem  19689  ordtrest2lem  19704  lmconst  19762  cndis  19792  pnrmopn  19844  cmpfi  19908  finptfin  20019  comppfsc  20033  ptbasfi  20082  pttoponconst  20098  ptcnplem  20122  pthaus  20139  xkoptsub  20155  xkopt  20156  nrmr0reg  20250  ordthmeolem  20302  fbssfi  20338  filcon  20384  hausflim  20482  cnpflf  20502  fclscf  20526  cnpfcf  20542  alexsublem  20544  ptcmplem2  20553  ptcmplem3  20554  tsmsfbas  20626  eltsms  20631  utopbas  20738  isucn2  20782  metutopOLD  21085  psmetutop  21086  nrginvrcn  21200  lebnumlem3  21463  fmcfil  21711  ovolicc2lem4  21931  mbfconst  22042  i1fmul  22103  itg2const  22147  itg2cnlem2  22169  itgle  22216  ibladdlem  22226  iblabs  22235  iblabsr  22236  iblmulc2  22237  bddmulibl  22245  ellimc2  22281  limcnlp  22282  c1lip1  22398  ply1nzb  22523  ulm0  22786  itgulm2  22804  dchrhash  23546  lgsquadlem2  23630  2sqlem10  23649  dchrisum  23677  rpvmasum2  23697  pntlemj  23788  axcontlem12  24278  uvtxnb  24497  usg2wlkeq2  24709  numclwwlkdisj  25080  rngoueqz  25432  ip2eqi  25772  ubthlem1  25786  hial2eq  26023  occon  26205  spanss  26266  pjnmopi  27067  ssmd1  27230  chrelat2i  27284  xrofsup  27582  ordtrest2NEWlem  27904  truae  28215  mbfmcst  28230  mbfmcnt  28239  dya2iocuni  28254  0rrv  28390  cvmliftlem15  28743  trpredss  29312  fin2so  30040  supadd  30042  ismblfin  30055  cnambfre  30063  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  iblabsnc  30079  iblmulc2nc  30080  bddiblnc  30085  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  neibastop2lem  30178  tailf  30193  filnetlem4  30199  frinfm  30226  sdclem1  30236  ssbnd  30284  hbtlem7  31074  itgoss  31112  itgpowd  31182  sumeq2ad  31566  prodeq2ad  31590  itgperiod  31780  stoweidlem35  31817  stoweidlem59  31841  fourierdlem31  31920  2reurex  32186  rmsupp0  32961  lincop  33009  lcoc0  33023  lssatle  34740  ltrneq2  35872  tendoeq2  36500
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-ral 2812
  Copyright terms: Public domain W3C validator