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

Theorem ralrimivw 2996
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 2994 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  2rmorex  3445  riinrab  4628  exse  5107  dmxp  5376  mpt2eq12  6757  ovmpt3rabdm  6934  offveqb  6961  exse2  7147  xpexgALT  7203  opabn1stprc  7272  mpt2exg  7290  uniqs  7850  boxriin  7992  fisupg  8249  fisup2g  8415  fisupcl  8416  fiinfg  8446  fiinf2g  8447  ordtypelem8  8471  wemapso2  8499  cantnflem1  8624  r1val1  8687  scottex  8786  dfac12k  9007  compssiso  9234  axcclem  9317  ondomon  9423  tskuni  9643  pinq  9787  supexpr  9914  dedekind  10238  supadd  11029  supmullem2  11032  zsupss  11815  qextlt  12072  qextle  12073  xrsupsslem  12175  xrinfmsslem  12176  supxrpnf  12186  ssnn0fi  12824  recan  14120  climconst  14318  sumeq2ad  14478  dvdsext  15090  smupvallem  15252  smumullem  15261  pc11  15631  prmreclem4  15670  vdwmc2  15730  vdwlem8  15739  vdwlem13  15744  cshwsex  15854  cshws0  15855  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdshom  16174  imasplusg  16224  imasmulr  16225  imasip  16228  imasaddvallem  16236  imasvscaf  16246  quslem  16250  divsfval  16254  mrcuni  16328  catideu  16383  homfeqd  16402  comfeqd  16414  2oppccomf  16432  catcoppccl  16805  lublecllem  17035  pmtrrn  17923  pmtrfrn  17924  gsummptif1n0  18411  evlseu  19564  ip2eq  20046  frlmup4  20188  pmatcollpw2lem  20630  basdif0  20805  clsval2  20902  neif  20952  ordtbaslem  21040  ordtrest2lem  21055  lmconst  21113  cndis  21143  pnrmopn  21195  cmpfi  21259  finptfin  21369  comppfsc  21383  ptbasfi  21432  pttoponconst  21448  ptcnplem  21472  pthaus  21489  xkoptsub  21505  xkopt  21506  nrmr0reg  21600  ordthmeolem  21652  fbssfi  21688  filconn  21734  hausflim  21832  cnpflf  21852  fclscf  21876  cnpfcf  21892  alexsublem  21895  ptcmplem2  21904  ptcmplem3  21905  tsmsfbas  21978  eltsms  21983  utopbas  22086  isucn2  22130  psmetutop  22419  nrginvrcn  22543  lebnumlem3  22809  fmcfil  23116  ovolicc2lem4  23334  mbfconst  23447  i1fmul  23508  itg2const  23552  itg2cnlem2  23574  itgle  23621  ibladdlem  23631  iblabs  23640  iblabsr  23641  iblmulc2  23642  bddmulibl  23650  ellimc2  23686  limcnlp  23687  c1lip1  23805  ply1nzb  23927  ulm0  24190  itgulm2  24208  dchrhash  25041  lgsquadlem2  25151  2sqlem10  25198  dchrisum  25226  rpvmasum2  25246  pntlemj  25337  axcontlem12  25900  nbgr0edg  26298  rusgr1vtx  26540  uspgr2wlkeq2  26599  clwwlknondisj  27086  clwwlknondisjOLD  27090  ip2eqi  27840  ubthlem1  27854  hial2eq  28091  occon  28274  spanss  28335  pjnmopi  29135  ssmd1  29298  chrelat2i  29352  xrofsup  29661  ordtrest2NEWlem  30096  prodindf  30213  truae  30434  mbfmcst  30449  mbfmcnt  30458  dya2iocuni  30473  0rrv  30641  hashreprin  30826  reprgt  30827  breprexplemc  30838  breprexp  30839  circlemeth  30846  hgt750lema  30863  cvmliftlem15  31406  trpredss  31853  neibastop2lem  32480  tailf  32495  filnetlem4  32501  fin2so  33526  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem26  33565  poimirlem28  33567  ismblfin  33580  cnambfre  33588  itg2addnclem  33591  itg2addnc  33594  itg2gt0cn  33595  ibladdnclem  33596  iblabsnc  33604  iblmulc2nc  33605  bddiblnc  33610  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  frinfm  33660  sdclem1  33669  ssbnd  33717  rngoueqz  33869  lssatle  34620  ltrneq2  35752  tendoeq2  36379  hbtlem7  38012  itgoss  38050  itgpowd  38117  trclrelexplem  38320  rfovcnvf1od  38615  dssmapf1od  38632  prodeq2ad  40142  0cnv  40292  itgperiod  40515  stoweidlem35  40570  stoweidlem59  40594  fourierdlem31  40673  subsaliuncllem  40893  subsaliuncl  40894  iundjiun  40995  hoiprodcl2  41090  ovnsslelem  41095  ovn0lem  41100  hoidmvlelem3  41132  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302  2reurex  41502  sprval  42054  rmsupp0  42474  lincop  42522  lcoc0  42536
  Copyright terms: Public domain W3C validator