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

Theorem ralrimivw 2879
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 25 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2876 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  2rmorex  3308  riinrab  4401  exse  4843  dmxp  5221  mpt2eq12  6341  ovmpt3rabdm  6519  offveqb  6546  exse2  6723  xpexgALT  6777  mpt2exg  6858  uniqs  7371  boxriin  7511  fisupg  7768  supmaxlem  7924  fisup2g  7926  fisupcl  7927  ordtypelem8  7950  wemapso2  7979  cantnflem1  8108  r1val1  8204  scottex  8303  dfac12k  8527  compssiso  8754  axcclem  8837  ondomon  8938  tskuni  9161  pinq  9305  supexpr  9432  dedekind  9743  supmullem2  10510  zsupss  11171  qextlt  11402  qextle  11403  xrsupsslem  11498  xrinfmsslem  11499  supxrpnf  11510  ssnn0fi  12062  recan  13132  climconst  13329  dvdsext  13896  smupvallem  13992  smumullem  14001  pc11  14262  prmreclem4  14296  vdwmc2  14356  vdwlem8  14365  vdwlem13  14370  cshwsex  14443  cshws0  14444  prdsplusg  14713  prdsmulr  14714  prdsvsca  14715  prdshom  14722  imasplusg  14772  imasmulr  14773  imasip  14776  imasaddvallem  14784  imasvscaf  14794  divslem  14798  divsfval  14802  mrcuni  14876  catideu  14930  homfeqd  14951  comfeqd  14963  2oppccomf  14981  catcoppccl  15293  lublecllem  15475  pmtrrn  16288  pmtrfrn  16289  gsummptif1n0  16796  evlseu  17984  ip2eq  18483  frlmup4  18630  pmatcollpw2lem  19073  basdif0  19249  clsval2  19345  neif  19395  ordtbaslem  19483  ordtrest2lem  19498  lmconst  19556  cndis  19586  pnrmopn  19638  cmpfi  19702  ptbasfi  19845  pttoponconst  19861  ptcnplem  19885  pthaus  19902  xkoptsub  19918  xkopt  19919  nrmr0reg  20013  ordthmeolem  20065  fbssfi  20101  filcon  20147  hausflim  20245  cnpflf  20265  fclscf  20289  cnpfcf  20305  alexsublem  20307  ptcmplem2  20316  ptcmplem3  20317  tsmsfbas  20389  eltsms  20394  utopbas  20501  isucn2  20545  metutopOLD  20848  psmetutop  20849  nrginvrcn  20963  lebnumlem3  21226  fmcfil  21474  ovolicc2lem4  21694  mbfconst  21805  i1fmul  21866  itg2const  21910  itg2cnlem2  21932  itgle  21979  ibladdlem  21989  iblabs  21998  iblabsr  21999  iblmulc2  22000  bddmulibl  22008  ellimc2  22044  limcnlp  22045  c1lip1  22161  ply1nzb  22286  ulm0  22548  itgulm2  22566  dchrhash  23302  lgsquadlem2  23386  2sqlem10  23405  dchrisum  23433  rpvmasum2  23453  pntlemj  23544  tgtrisegint  23646  axcontlem12  23982  elntg  23991  uvtxnb  24201  usg2wlkeq2  24413  numclwwlkdisj  24785  rngoueqz  25136  ip2eqi  25476  ubthlem1  25490  hial2eq  25727  occon  25909  spanss  25970  pjnmopi  26771  ssmd1  26934  chrelat2i  26988  fcnvgreu  27214  xrofsup  27278  submarchi  27420  ordtrest2NEWlem  27568  truae  27883  mbfmcst  27898  mbfmcnt  27907  dya2iocuni  27922  sseqf  27999  0rrv  28058  signsvvfval  28203  cvmliftlem15  28411  trpredss  28917  fin2so  29645  supadd  29647  ismblfin  29660  cnambfre  29668  itg2addnclem  29671  itg2addnc  29674  itg2gt0cn  29675  ibladdnclem  29676  iblabsnc  29684  iblmulc2nc  29685  bddiblnc  29690  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  finptfin  29797  comppfsc  29807  neibastop2lem  29809  tailf  29824  filnetlem4  29830  frinfm  29857  sdclem1  29867  ssbnd  29915  hbtlem7  30706  itgoss  30745  itgpowd  30815  stoweidlem35  31363  stoweidlem59  31387  fourierdlem83  31518  fourierdlem108  31543  2reurex  31681  rmsupp0  32060  lincop  32108  lcoc0  32122  lssatle  33830  ltrneq2  34962  tendoeq2  35588
  Copyright terms: Public domain W3C validator