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

Theorem ralrimivw 2750
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 23 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2748 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   A.wral 2666
This theorem is referenced by:  2rmorex  3098  riinrab  4126  exse  4506  dmxp  5047  exse2  5197  mpt2eq12  6093  xpexgALT  6256  offveqb  6285  mpt2exg  6382  uniqs  6923  boxriin  7063  fisupg  7314  supmaxlem  7425  fisup2g  7427  fisupcl  7428  ordtypelem8  7450  r1val1  7668  scottex  7765  dfac12k  7983  compssiso  8210  axcclem  8293  ondomon  8394  tskuni  8614  pinq  8760  supexpr  8887  supmullem2  9931  zsupss  10521  qextlt  10745  qextle  10746  xrsupsslem  10841  xrinfmsslem  10842  supxrpnf  10853  recan  12095  climconst  12292  dvdsext  12855  smupvallem  12950  smumullem  12959  pc11  13208  prmreclem4  13242  vdwmc2  13302  vdwlem8  13311  vdwlem13  13316  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdshom  13644  imasplusg  13698  imasmulr  13699  imasaddvallem  13709  imasvscaf  13719  divslem  13723  divsfval  13727  mrcuni  13801  catideu  13855  homfeqd  13876  comfeqd  13888  2oppccomf  13906  catcoppccl  14218  lubid  14394  ip2eq  16839  basdif0  16973  clsval2  17069  neif  17119  ordtbaslem  17206  ordtrest2lem  17221  lmconst  17279  cndis  17309  pnrmopn  17361  cmpfi  17425  ptbasfi  17566  pttoponconst  17582  ptcnplem  17606  pthaus  17623  xkoptsub  17639  xkopt  17640  nrmr0reg  17734  ordthmeolem  17786  fbssfi  17822  filcon  17868  hausflim  17966  cnpflf  17986  fclscf  18010  cnpfcf  18026  alexsublem  18028  ptcmplem2  18037  ptcmplem3  18038  tsmsfbas  18110  eltsms  18115  utopbas  18218  isucn2  18262  metutopOLD  18565  psmetutop  18566  nrginvrcn  18680  lebnumlem3  18941  fmcfil  19178  ovolicc2lem4  19369  mbfconst  19480  i1fmul  19541  itg2const  19585  itg2cnlem2  19607  itgle  19654  ibladdlem  19664  iblabs  19673  iblabsr  19674  iblmulc2  19675  bddmulibl  19683  ellimc2  19717  limcnlp  19718  c1lip1  19834  evlseu  19890  ply1nzb  19998  ulm0  20260  itgulm2  20278  dchrhash  21008  lgsquadlem2  21092  2sqlem10  21111  dchrisum  21139  rpvmasum2  21159  pntlemj  21250  rngoueqz  21971  ip2eqi  22311  ubthlem1  22325  hial2eq  22561  occon  22742  spanss  22803  pjnmopi  23604  ssmd1  23767  chrelat2i  23821  xrofsup  24079  truae  24547  mbfmcst  24562  mbfmcnt  24571  dya2iocuni  24586  0rrv  24662  cvmliftlem15  24938  dedekind  25140  trpredss  25446  axcontlem12  25818  supadd  26138  ismblfin  26146  cnambfre  26154  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  finptfin  26267  comppfsc  26277  neibastop2lem  26279  tailf  26294  filnetlem4  26300  frinfm  26327  sdclem1  26337  ssbnd  26387  frlmup4  27121  hbtlem7  27197  itgoss  27236  pmtrrn  27267  pmtrfrn  27268  stoweidlem35  27651  stoweidlem59  27675  2reurex  27826  lssatle  29498  ltrneq2  30630  tendoeq2  31256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2671
  Copyright terms: Public domain W3C validator