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

Theorem ralrimivw 2949
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:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2947 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-ral 2900
This theorem is referenced by:  2rmorex  3378  riinrab  4526  exse  4992  dmxp  5252  mpt2eq12  6591  ovmpt3rabdm  6767  offveqb  6794  exse2  6975  xpexgALT  7029  mpt2exg  7111  uniqs  7671  boxriin  7813  fisupg  8070  fisup2g  8234  fisupcl  8235  fiinfg  8265  fiinf2g  8266  ordtypelem8  8290  wemapso2  8318  cantnflem1  8446  r1val1  8509  scottex  8608  dfac12k  8829  compssiso  9056  axcclem  9139  ondomon  9241  tskuni  9461  pinq  9605  supexpr  9732  dedekind  10051  supadd  10838  supmullem2  10841  zsupss  11609  qextlt  11867  qextle  11868  xrsupsslem  11965  xrinfmsslem  11966  supxrpnf  11976  ssnn0fi  12601  recan  13870  climconst  14068  dvdsext  14827  smupvallem  14989  smumullem  14998  pc11  15368  prmreclem4  15407  vdwmc2  15467  vdwlem8  15476  vdwlem13  15481  cshwsex  15591  cshws0  15592  prdsplusg  15887  prdsmulr  15888  prdsvsca  15889  prdshom  15896  imasplusg  15946  imasmulr  15947  imasip  15950  imasaddvallem  15958  imasvscaf  15968  quslem  15972  divsfval  15976  mrcuni  16050  catideu  16105  homfeqd  16124  comfeqd  16136  2oppccomf  16154  catcoppccl  16527  lublecllem  16757  pmtrrn  17646  pmtrfrn  17647  gsummptif1n0  18134  evlseu  19283  ip2eq  19762  frlmup4  19901  pmatcollpw2lem  20343  basdif0  20510  clsval2  20606  neif  20656  ordtbaslem  20744  ordtrest2lem  20759  lmconst  20817  cndis  20847  pnrmopn  20899  cmpfi  20963  finptfin  21073  comppfsc  21087  ptbasfi  21136  pttoponconst  21152  ptcnplem  21176  pthaus  21193  xkoptsub  21209  xkopt  21210  nrmr0reg  21304  ordthmeolem  21356  fbssfi  21393  filcon  21439  hausflim  21537  cnpflf  21557  fclscf  21581  cnpfcf  21597  alexsublem  21600  ptcmplem2  21609  ptcmplem3  21610  tsmsfbas  21683  eltsms  21688  utopbas  21791  isucn2  21835  psmetutop  22123  nrginvrcn  22239  lebnumlem3  22501  fmcfil  22796  ovolicc2lem4  23012  mbfconst  23125  i1fmul  23186  itg2const  23230  itg2cnlem2  23252  itgle  23299  ibladdlem  23309  iblabs  23318  iblabsr  23319  iblmulc2  23320  bddmulibl  23328  ellimc2  23364  limcnlp  23365  c1lip1  23481  ply1nzb  23603  ulm0  23866  itgulm2  23884  dchrhash  24713  lgsquadlem2  24823  2sqlem10  24870  dchrisum  24898  rpvmasum2  24918  pntlemj  25009  axcontlem12  25573  uvtxnb  25791  usg2wlkeq2  26003  numclwwlkdisj  26373  ip2eqi  26902  ubthlem1  26916  hial2eq  27153  occon  27336  spanss  27397  pjnmopi  28197  ssmd1  28360  chrelat2i  28414  xrofsup  28729  ordtrest2NEWlem  29102  truae  29439  mbfmcst  29454  mbfmcnt  29463  dya2iocuni  29478  0rrv  29646  cvmliftlem15  30340  trpredss  30779  neibastop2lem  31331  tailf  31346  filnetlem4  31352  fin2so  32362  matunitlindflem1  32371  matunitlindflem2  32372  poimirlem26  32401  poimirlem28  32403  ismblfin  32416  cnambfre  32424  itg2addnclem  32427  itg2addnc  32430  itg2gt0cn  32431  ibladdnclem  32432  iblabsnc  32440  iblmulc2nc  32441  bddiblnc  32446  ftc1anclem6  32456  ftc1anclem7  32457  ftc1anclem8  32458  ftc1anc  32459  frinfm  32496  sdclem1  32505  ssbnd  32553  rngoueqz  32705  lssatle  33116  ltrneq2  34248  tendoeq2  34876  hbtlem7  36510  itgoss  36548  itgpowd  36615  trclrelexplem  36818  rfovcnvf1od  37114  dssmapf1od  37131  sumeq2ad  38429  prodeq2ad  38456  itgperiod  38670  stoweidlem35  38725  stoweidlem59  38749  fourierdlem31  38828  subsaliuncllem  39048  subsaliuncl  39049  iundjiun  39150  hoiprodcl2  39242  ovnsslelem  39247  ovn0lem  39252  hoidmvlelem3  39284  smflimlem1  39454  smflimlem2  39455  smflimlem3  39456  2reurex  39627  opabn1stprc  40126  nbgr0edg  40574  rusgr1vtx  40783  uspgr2wlkeq2  40850  clwwlksndisj  41275  frgrhash2wsp  41492  rmsupp0  41938  lincop  41986  lcoc0  42000
  Copyright terms: Public domain W3C validator