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

Theorem ralrimivw 3170
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 3168 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  wral 3125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911
This theorem depends on definitions:  df-bi 209  df-ral 3130
This theorem is referenced by:  r19.27v  3171  r19.28v  3173  r19.37v  3331  2rmorex  3725  2reurex  3730  riinrab  4982  exse  5495  dmxp  5775  mpoeq12  7204  ovmpt3rabdm  7382  offveqb  7409  exse2  7600  xpexgALT  7660  opabn1stprc  7734  mpoexg  7752  uniqs  8335  boxriin  8482  fisupg  8744  fisup2g  8910  fisupcl  8911  fiinfg  8941  fiinf2g  8942  ordtypelem8  8967  wemapso2  8995  cantnflem1  9130  r1val1  9193  scottex  9292  updjud  9341  dfac12k  9551  compssiso  9774  axcclem  9857  ondomon  9963  tskuni  10183  pinq  10327  supexpr  10454  dedekind  10781  supadd  11587  supmullem2  11590  zsupss  12316  qextlt  12575  qextle  12576  xrsupsslem  12679  xrinfmsslem  12680  supxrpnf  12690  ssnn0fi  13337  recan  14676  climconst  14880  sumeq2sdv  15041  dvdsext  15651  smupvallem  15810  smumullem  15819  pc11  16194  prmreclem4  16233  vdwmc2  16293  vdwlem8  16302  vdwlem13  16307  cshwsex  16413  cshws0  16414  prdsplusg  16710  prdsmulr  16711  prdsvsca  16712  prdshom  16719  imasplusg  16769  imasmulr  16770  imasip  16773  imasaddvallem  16781  imasvscaf  16791  quslem  16795  divsfval  16799  mrcuni  16871  catideu  16925  homfeqd  16944  comfeqd  16956  2oppccomf  16974  catcoppccl  17347  lublecllem  17577  pmtrrn  18564  pmtrfrn  18565  gsummptif1n0  19065  evlseu  20272  ip2eq  20773  frlmup4  20921  pmatcollpw2lem  21361  basdif0  21537  clsval2  21634  neif  21684  ordtbaslem  21772  ordtrest2lem  21787  lmconst  21845  cndis  21875  pnrmopn  21927  cmpfi  21992  finptfin  22102  comppfsc  22116  ptbasfi  22165  pttoponconst  22181  ptcnplem  22205  pthaus  22222  xkoptsub  22238  xkopt  22239  nrmr0reg  22333  ordthmeolem  22385  fbssfi  22421  filconn  22467  hausflim  22565  cnpflf  22585  fclscf  22609  cnpfcf  22625  alexsublem  22628  ptcmplem2  22637  ptcmplem3  22638  tsmsfbas  22712  eltsms  22717  utopbas  22820  isucn2  22864  psmetutop  23153  nrginvrcn  23277  lebnumlem3  23547  fmcfil  23855  ovolicc2lem4  24103  mbfconst  24216  i1fmul  24279  itg2const  24323  itg2cnlem2  24345  itgle  24392  ibladdlem  24402  iblabs  24411  iblabsr  24412  iblmulc2  24413  bddmulibl  24421  bddiblnc  24424  ellimc2  24459  limcnlp  24460  c1lip1  24579  itgpowd  24632  ply1nzb  24702  ulm0  24965  itgulm2  24983  dchrhash  25834  lgsquadlem2  25944  2sqlem10  25991  dchrisum  26055  rpvmasum2  26075  pntlemj  26166  axcontlem12  26748  nbgr0edg  27126  rusgr1vtx  27357  uspgr2wlkeq2  27415  clwwlknondisj  27875  ip2eqi  28618  ubthlem1  28632  hial2eq  28868  occon  29049  spanss  29110  pjnmopi  29910  ssmd1  30073  chrelat2i  30127  xrofsup  30479  ordtrest2NEWlem  31173  prodindf  31290  truae  31510  mbfmcst  31525  mbfmcnt  31534  dya2iocuni  31549  0rrv  31717  hashreprin  31899  reprgt  31900  breprexplemc  31911  breprexp  31912  circlemeth  31919  hgt750lema  31936  cvmliftlem15  32553  satf0suclem  32630  fmla0disjsuc  32653  fmlasucdisj  32654  trpredss  33076  neibastop2lem  33716  tailf  33731  filnetlem4  33737  fin2so  34920  matunitlindflem1  34929  matunitlindflem2  34930  poimirlem26  34959  poimirlem28  34961  ismblfin  34974  cnambfre  34981  itg2addnclem  34984  itg2addnc  34987  itg2gt0cn  34988  ibladdnclem  34989  iblabsnc  34997  iblmulc2nc  34998  ftc1anclem6  35011  ftc1anclem7  35012  ftc1anclem8  35013  ftc1anc  35014  frinfm  35049  sdclem1  35057  ssbnd  35102  rngoueqz  35254  lssatle  36187  ltrneq2  37320  tendoeq2  37946  lcmineqlem12  39192  hbtlem7  39862  itgoss  39900  trclrelexplem  40191  rfovcnvf1od  40485  dssmapf1od  40502  neik0pk1imk0  40532  collexd  40748  prodeq2ad  42025  0cnv  42175  itgperiod  42414  stoweidlem35  42468  stoweidlem59  42492  fourierdlem31  42571  subsaliuncllem  42788  subsaliuncl  42789  iundjiun  42890  hoiprodcl2  42985  ovnsslelem  42990  ovn0lem  42995  hoidmvlelem3  43027  smflimlem1  43195  smflimlem2  43196  smflimlem3  43197  fundcmpsurinjlem2  43707  sprval  43787  prprval  43822  rmsupp0  44561  lincop  44608  lcoc0  44622
  Copyright terms: Public domain W3C validator