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

Theorem ralrimivw 2602
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 2600 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2518
This theorem is referenced by:  2rmorex  2944  riinrab  3951  exse  4329  dmxp  4885  exse2  5035  mpt2eq12  5842  xpexgALT  6004  offveqb  6033  mpt2exg  6130  uniqs  6687  boxriin  6826  fisupg  7073  supmaxlem  7183  fisup2g  7185  fisupcl  7186  ordtypelem8  7208  r1val1  7426  scottex  7523  dfac12k  7741  compssiso  7968  axcclem  8051  ondomon  8153  tskuni  8373  pinq  8519  supexpr  8646  lbinfm  9675  supmullem2  9689  zsupss  10274  qextlt  10496  qextle  10497  xrsupsslem  10591  xrinfmsslem  10592  supxrpnf  10603  recan  11785  climconst  11982  dvdsext  12541  smupvallem  12636  smumullem  12645  pc11  12894  prmreclem4  12928  vdwmc2  12988  vdwlem8  12997  vdwlem13  13002  prdsplusg  13320  prdsmulr  13321  prdsvsca  13322  prdshom  13328  imasplusg  13382  imasmulr  13383  imasaddvallem  13393  imasvscaf  13403  divslem  13407  divsfval  13411  mrcuni  13485  catideu  13539  homfeqd  13560  comfeqd  13572  2oppccomf  13590  catcoppccl  13902  lubid  14078  dprdval  15200  ip2eq  16519  basdif0  16653  clsval2  16749  neif  16799  ordtbaslem  16880  ordtrest2lem  16895  lmconst  16953  cndis  16981  pnrmopn  17033  cmpfi  17097  elpt  17229  elptr  17230  ptbasfi  17238  pttoponconst  17254  dfac14  17274  ptcnplem  17277  pthaus  17294  xkoptsub  17310  xkopt  17311  nrmr0reg  17402  ordthmeolem  17454  fbssfi  17494  filcon  17540  hausflim  17638  cnpflf  17658  fclscf  17682  cnpfcf  17698  alexsublem  17700  ptcmplem2  17709  ptcmplem3  17710  tsmsfbas  17772  eltsms  17777  nrginvrcn  18164  lebnumlem3  18423  fmcfil  18660  ovolicc2lem4  18841  mbfconst  18952  i1fmul  19013  itg2const  19057  itg2cnlem2  19079  itgle  19126  ibladdlem  19136  iblabs  19145  iblabsr  19146  iblmulc2  19147  bddmulibl  19155  ellimc2  19189  limcnlp  19190  c1lip1  19306  evlseu  19362  ply1nzb  19470  ulm0  19732  itgulm2  19747  dchrhash  20472  lgsquadlem2  20556  2sqlem10  20575  dchrisum  20603  rpvmasum2  20623  pntlemj  20714  rngoueqz  21057  ip2eqi  21395  ubthlem1  21409  hial2eq  21645  occon  21826  spanss  21887  pjnmopi  22688  ssmd1  22851  chrelat2i  22905  cvmliftlem15  23201  dedekind  23453  trpredss  23601  axcontlem12  23978  eqfnung2  24485  mapmapmap  24515  istopx  24914  finptfin  25664  comppfsc  25674  neibastop2lem  25676  tailf  25691  filnetlem4  25697  frinfm  25783  sdclem1  25820  ssbnd  25879  frlmup4  26620  hbtlem7  26696  itgoss  26735  pmtrrn  26766  pmtrfrn  26767  lssatle  28372  ltrneq2  29504  tendoeq2  30130
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 2523
  Copyright terms: Public domain W3C validator