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

Theorem ralrimivw 2838
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralrimivw  |-  ( ph  ->  A. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3  |-  ( ph  ->  ps )
21a1d 26 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2835 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-ral 2778
This theorem is referenced by:  2rmorex  3273  riinrab  4369  exse  4809  dmxp  5064  mpt2eq12  6356  ovmpt3rabdm  6531  offveqb  6558  exse2  6737  xpexgALT  6791  mpt2exg  6873  uniqs  7422  boxriin  7563  fisupg  7816  supmaxlemOLD  7979  fisup2g  7981  fisupcl  7982  ordtypelem8  8031  wemapso2  8059  cantnflem1  8184  r1val1  8247  scottex  8346  dfac12k  8566  compssiso  8793  axcclem  8876  ondomon  8977  tskuni  9197  pinq  9341  supexpr  9468  dedekind  9786  supadd  10564  supmullem2  10567  zsupss  11242  qextlt  11485  qextle  11486  xrsupsslem  11581  xrinfmsslem  11582  supxrpnf  11593  ssnn0fi  12183  recan  13367  climconst  13574  dvdsext  14323  smupvallem  14420  smumullem  14429  pc11  14789  prmreclem4  14823  vdwmc2  14889  vdwlem8  14898  vdwlem13  14903  cshwsex  15031  cshws0  15032  prdsplusg  15316  prdsmulr  15317  prdsvsca  15318  prdshom  15325  imasplusg  15375  imasmulr  15376  imasip  15379  imasaddvallem  15387  imasvscaf  15397  quslem  15401  divsfval  15405  mrcuni  15479  catideu  15533  homfeqd  15552  comfeqd  15564  2oppccomf  15582  catcoppccl  15955  lublecllem  16186  pmtrrn  17050  pmtrfrn  17051  gsummptif1n0  17539  evlseu  18680  ip2eq  19157  frlmup4  19296  pmatcollpw2lem  19738  basdif0  19905  clsval2  20002  neif  20053  ordtbaslem  20141  ordtrest2lem  20156  lmconst  20214  cndis  20244  pnrmopn  20296  cmpfi  20360  finptfin  20470  comppfsc  20484  ptbasfi  20533  pttoponconst  20549  ptcnplem  20573  pthaus  20590  xkoptsub  20606  xkopt  20607  nrmr0reg  20701  ordthmeolem  20753  fbssfi  20789  filcon  20835  hausflim  20933  cnpflf  20953  fclscf  20977  cnpfcf  20993  alexsublem  20996  ptcmplem2  21005  ptcmplem3  21006  tsmsfbas  21079  eltsms  21084  utopbas  21187  isucn2  21231  psmetutop  21519  nrginvrcn  21631  lebnumlem3  21913  fmcfil  22161  ovolicc2lem4OLD  22380  ovolicc2lem4  22381  mbfconst  22498  i1fmul  22561  itg2const  22605  itg2cnlem2  22627  itgle  22674  ibladdlem  22684  iblabs  22693  iblabsr  22694  iblmulc2  22695  bddmulibl  22703  ellimc2  22739  limcnlp  22740  c1lip1  22856  ply1nzb  22978  ulm0  23250  itgulm2  23268  dchrhash  24101  lgsquadlem2  24185  2sqlem10  24204  dchrisum  24232  rpvmasum2  24252  pntlemj  24343  axcontlem12  24892  uvtxnb  25111  usg2wlkeq2  25323  numclwwlkdisj  25694  rngoueqz  26044  ip2eqi  26384  ubthlem1  26398  hial2eq  26635  occon  26816  spanss  26877  pjnmopi  27677  ssmd1  27840  chrelat2i  27894  xrofsup  28230  ordtrest2NEWlem  28608  truae  28946  mbfmcst  28961  mbfmcnt  28970  dya2iocuni  28985  0rrv  29151  cvmliftlem15  29850  trpredss  30298  neibastop2lem  30842  tailf  30857  filnetlem4  30863  fin2so  31680  poimirlem26  31714  poimirlem28  31716  ismblfin  31729  cnambfre  31737  itg2addnclem  31741  itg2addnc  31744  itg2gt0cn  31745  ibladdnclem  31746  iblabsnc  31754  iblmulc2nc  31755  bddiblnc  31760  ftc1anclem6  31770  ftc1anclem7  31771  ftc1anclem8  31772  ftc1anc  31773  frinfm  31810  sdclem1  31820  ssbnd  31868  lssatle  32334  ltrneq2  33466  tendoeq2  34094  hbtlem7  35738  itgoss  35776  itgpowd  35846  trclrelexplem  35990  sumeq2ad  37267  prodeq2ad  37292  itgperiod  37475  stoweidlem35  37513  stoweidlem59  37537  fourierdlem31  37617  iundjiun  37855  2reurex  38050  rmsupp0  38970  lincop  39018  lcoc0  39032
  Copyright terms: Public domain W3C validator