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

Theorem ralrimivw 2640
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 2638 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  2rmorex  2982  riinrab  3993  exse  4373  dmxp  4913  exse2  5063  mpt2eq12  5924  xpexgALT  6086  offveqb  6115  mpt2exg  6212  uniqs  6735  boxriin  6874  fisupg  7121  supmaxlem  7231  fisup2g  7233  fisupcl  7234  ordtypelem8  7256  r1val1  7474  scottex  7571  dfac12k  7789  compssiso  8016  axcclem  8099  ondomon  8201  tskuni  8421  pinq  8567  supexpr  8694  lbinfm  9723  supmullem2  9737  zsupss  10323  qextlt  10546  qextle  10547  xrsupsslem  10641  xrinfmsslem  10642  supxrpnf  10653  recan  11836  climconst  12033  dvdsext  12595  smupvallem  12690  smumullem  12699  pc11  12948  prmreclem4  12982  vdwmc2  13042  vdwlem8  13051  vdwlem13  13056  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  imasplusg  13436  imasmulr  13437  imasaddvallem  13447  imasvscaf  13457  divslem  13461  divsfval  13465  mrcuni  13539  catideu  13593  homfeqd  13614  comfeqd  13626  2oppccomf  13644  catcoppccl  13956  lubid  14132  dprdval  15254  ip2eq  16573  basdif0  16707  clsval2  16803  neif  16853  ordtbaslem  16934  ordtrest2lem  16949  lmconst  17007  cndis  17035  pnrmopn  17087  cmpfi  17151  elpt  17283  elptr  17284  ptbasfi  17292  pttoponconst  17308  dfac14  17328  ptcnplem  17331  pthaus  17348  xkoptsub  17364  xkopt  17365  nrmr0reg  17456  ordthmeolem  17508  fbssfi  17548  filcon  17594  hausflim  17692  cnpflf  17712  fclscf  17736  cnpfcf  17752  alexsublem  17754  ptcmplem2  17763  ptcmplem3  17764  tsmsfbas  17826  eltsms  17831  nrginvrcn  18218  lebnumlem3  18477  fmcfil  18714  ovolicc2lem4  18895  mbfconst  19006  i1fmul  19067  itg2const  19111  itg2cnlem2  19133  itgle  19180  ibladdlem  19190  iblabs  19199  iblabsr  19200  iblmulc2  19201  bddmulibl  19209  ellimc2  19243  limcnlp  19244  c1lip1  19360  evlseu  19416  ply1nzb  19524  ulm0  19786  itgulm2  19801  dchrhash  20526  lgsquadlem2  20610  2sqlem10  20629  dchrisum  20657  rpvmasum2  20677  pntlemj  20768  rngoueqz  21113  ip2eqi  21451  ubthlem1  21465  hial2eq  21701  occon  21882  spanss  21943  pjnmopi  22744  ssmd1  22907  chrelat2i  22961  xrofsup  23270  imambfm  23582  mbfmcnt  23588  itgmeq123dTMP  23604  cvmliftlem15  23844  dedekind  24097  trpredss  24303  axcontlem12  24675  supadd  24996  itg2gt0cn  25006  ibladdnclem  25007  iblabsnc  25015  iblmulc2nc  25016  bddiblnc  25021  eqfnung2  25221  mapmapmap  25251  istopx  25650  finptfin  26400  comppfsc  26410  neibastop2lem  26412  tailf  26427  filnetlem4  26433  frinfm  26519  sdclem1  26556  ssbnd  26615  frlmup4  27356  hbtlem7  27432  itgoss  27471  pmtrrn  27502  pmtrfrn  27503  2reurex  28062  lssatle  29827  ltrneq2  30959  tendoeq2  31585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator