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

Theorem ralrimivw 2589
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 24 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2587 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2509
This theorem is referenced by:  riinrab  3875  exse  4250  dmxp  4804  exse2  4954  mpt2eq12  5760  xpexgALT  5922  offveqb  5951  mpt2exg  6048  uniqs  6605  boxriin  6744  fisupg  6990  supmaxlem  7099  fisup2g  7101  fisupcl  7102  ordtypelem8  7124  r1val1  7342  scottex  7439  dfac12k  7657  compssiso  7884  axcclem  7967  ondomon  8067  tskuni  8285  pinq  8431  supexpr  8558  lbinfm  9587  supmullem2  9601  zsupss  10186  qextlt  10408  qextle  10409  xrsupsslem  10503  xrinfmsslem  10504  supxrpnf  10515  recan  11697  climconst  11894  dvdsext  12453  smupvallem  12548  smumullem  12557  pc11  12806  prmreclem4  12840  vdwmc2  12900  vdwlem8  12909  vdwlem13  12914  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdshom  13240  imasplusg  13294  imasmulr  13295  imasaddvallem  13305  imasvscaf  13315  divslem  13319  divsfval  13323  mrcuni  13395  homfeqd  13442  comfeqd  13454  2oppccomf  13472  catcoppccl  13784  lubid  13960  dprdval  15073  ip2eq  16389  basdif0  16523  clsval2  16619  neif  16669  ordtbaslem  16750  ordtrest2lem  16765  lmconst  16823  cndis  16851  pnrmopn  16903  cmpfi  16967  elpt  17099  elptr  17100  ptbasfi  17108  pttoponconst  17124  dfac14  17144  ptcnplem  17147  pthaus  17164  xkoptsub  17180  xkopt  17181  nrmr0reg  17272  ordthmeolem  17324  fbssfi  17364  filcon  17410  hausflim  17508  cnpflf  17528  fclscf  17552  cnpfcf  17568  alexsublem  17570  ptcmplem2  17579  ptcmplem3  17580  tsmsfbas  17642  eltsms  17647  nrginvrcn  18034  lebnumlem3  18293  fmcfil  18530  ovolicc2lem4  18711  mbfconst  18822  i1fmul  18883  itg2const  18927  itg2cnlem2  18949  itgle  18996  ibladdlem  19006  iblabs  19015  iblabsr  19016  iblmulc2  19017  bddmulibl  19025  ellimc2  19059  limcnlp  19060  c1lip1  19176  ply1nzb  19340  ulm0  19602  itgulm2  19617  dchrhash  20342  lgsquadlem2  20426  2sqlem10  20445  dchrisum  20473  rpvmasum2  20493  pntlemj  20584  rngoueqz  20927  ip2eqi  21265  ubthlem1  21279  hial2eq  21515  occon  21696  spanss  21757  pjnmopi  22558  ssmd1  22721  chrelat2i  22775  cvmliftlem15  23000  dedekind  23252  trpredss  23400  axcontlem12  23777  eqfnung2  24284  mapmapmap  24314  istopx  24713  finptfin  25463  comppfsc  25473  neibastop2lem  25475  tailf  25490  filnetlem4  25496  frinfm  25582  sdclem1  25619  ssbnd  25678  hbtlem7  26495  itgoss  26534  pmtrrn  26565  pmtrfrn  26566  lssatle  28109  ltrneq2  29241  tendoeq2  29867
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540  df-ral 2513
  Copyright terms: Public domain W3C validator