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

Theorem ralrimivw 2627
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 22 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2625 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543
This theorem is referenced by:  2rmorex  2969  riinrab  3977  exse  4357  dmxp  4897  exse2  5047  mpt2eq12  5908  xpexgALT  6070  offveqb  6099  mpt2exg  6196  uniqs  6719  boxriin  6858  fisupg  7105  supmaxlem  7215  fisup2g  7217  fisupcl  7218  ordtypelem8  7240  r1val1  7458  scottex  7555  dfac12k  7773  compssiso  8000  axcclem  8083  ondomon  8185  tskuni  8405  pinq  8551  supexpr  8678  lbinfm  9707  supmullem2  9721  zsupss  10307  qextlt  10530  qextle  10531  xrsupsslem  10625  xrinfmsslem  10626  supxrpnf  10637  recan  11820  climconst  12017  dvdsext  12579  smupvallem  12674  smumullem  12683  pc11  12932  prmreclem4  12966  vdwmc2  13026  vdwlem8  13035  vdwlem13  13040  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  imasplusg  13420  imasmulr  13421  imasaddvallem  13431  imasvscaf  13441  divslem  13445  divsfval  13449  mrcuni  13523  catideu  13577  homfeqd  13598  comfeqd  13610  2oppccomf  13628  catcoppccl  13940  lubid  14116  dprdval  15238  ip2eq  16557  basdif0  16691  clsval2  16787  neif  16837  ordtbaslem  16918  ordtrest2lem  16933  lmconst  16991  cndis  17019  pnrmopn  17071  cmpfi  17135  elpt  17267  elptr  17268  ptbasfi  17276  pttoponconst  17292  dfac14  17312  ptcnplem  17315  pthaus  17332  xkoptsub  17348  xkopt  17349  nrmr0reg  17440  ordthmeolem  17492  fbssfi  17532  filcon  17578  hausflim  17676  cnpflf  17696  fclscf  17720  cnpfcf  17736  alexsublem  17738  ptcmplem2  17747  ptcmplem3  17748  tsmsfbas  17810  eltsms  17815  nrginvrcn  18202  lebnumlem3  18461  fmcfil  18698  ovolicc2lem4  18879  mbfconst  18990  i1fmul  19051  itg2const  19095  itg2cnlem2  19117  itgle  19164  ibladdlem  19174  iblabs  19183  iblabsr  19184  iblmulc2  19185  bddmulibl  19193  ellimc2  19227  limcnlp  19228  c1lip1  19344  evlseu  19400  ply1nzb  19508  ulm0  19770  itgulm2  19785  dchrhash  20510  lgsquadlem2  20594  2sqlem10  20613  dchrisum  20641  rpvmasum2  20661  pntlemj  20752  rngoueqz  21097  ip2eqi  21435  ubthlem1  21449  hial2eq  21685  occon  21866  spanss  21927  pjnmopi  22728  ssmd1  22891  chrelat2i  22945  xrofsup  23255  imambfm  23567  mbfmcnt  23573  itgmeq123dTMP  23589  cvmliftlem15  23829  dedekind  24082  trpredss  24232  axcontlem12  24603  eqfnung2  25118  mapmapmap  25148  istopx  25547  finptfin  26297  comppfsc  26307  neibastop2lem  26309  tailf  26324  filnetlem4  26330  frinfm  26416  sdclem1  26453  ssbnd  26512  frlmup4  27253  hbtlem7  27329  itgoss  27368  pmtrrn  27399  pmtrfrn  27400  2reurex  27959  lssatle  29205  ltrneq2  30337  tendoeq2  30963
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator