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

Theorem ralrimi 2637
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
Hypotheses
Ref Expression
ralrimi.1  |-  F/ x ph
ralrimi.2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
Assertion
Ref Expression
ralrimi  |-  ( ph  ->  A. x  e.  A  ps )

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3  |-  F/ x ph
2 ralrimi.2 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2alrimi 1757 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2561 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 203 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   F/wnf 1534    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralrimiv  2638  reximdai  2664  r19.12  2669  rexlimd  2677  rexlimd2  2678  r19.37  2702  ralcom2  2717  2rmorex  2982  iineq2d  3941  disjxiun  4036  mpteq2da  4121  reusv6OLD  4561  mpteqb  5630  zfrep6  5764  eusvobj2  6353  riotasv3dOLD  6370  tfr3  6431  tz7.49  6473  mapxpen  7043  dfac2  7773  hsmexlem4  8071  axcc3  8080  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  ac6num  8122  zindd  10129  mreexexd  13566  ptcnplem  17331  xkocnv  17521  itg2splitlem  19119  itg2split  19120  itgeq1f  19142  funimass4f  23058  fmptdF  23236  fcomptf  23245  offval2f  23248  funcnvmptOLD  23249  funcnvmpt  23250  isoun  23257  esumeq12dvaf  23429  esumel  23441  esumf1o  23444  esumc  23445  esumlef  23450  esumpinfval  23456  esumpinfsum  23460  measinblem  23562  dstrvprob  23687  untsucf  24071  dedekind  24097  dedekindle  24098  trpredmintr  24305  wfrlem4  24330  frrlem4  24355  mptelee  24595  svli2  25587  cmpmon  25918  cover2  26461  upixp  26506  indexdom  26516  filbcmb  26535  sdclem2  26555  eq0rabdioph  26959  eqrabdioph  26960  setindtr  27220  rzalf  27791  fsumcnf  27795  fnchoice  27803  refsumcn  27804  rfcnnnub  27810  refsum2cnlem1  27811  fmptdf  27821  clim1fr1  27830  climsuse  27837  stoweidlem5  27857  stoweidlem16  27868  stoweidlem17  27869  stoweidlem18  27870  stoweidlem19  27871  stoweidlem21  27873  stoweidlem26  27878  stoweidlem27  27879  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem36  27888  stoweidlem41  27893  stoweidlem42  27894  stoweidlem44  27896  stoweidlem45  27897  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem55  27907  stoweidlem59  27911  stoweidlem60  27912  stoweidlem61  27913  stoweidlem62  27914  stoweid  27915  wallispilem3  27919  stirlinglem5  27930  stirlinglem13  27938  bnj1379  29179  bnj1145  29339  bnj1204  29358  bnj1388  29379  bnj1417  29387  bnj1489  29402
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