Theorem ralrimi 2797

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

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 |- F/ x ph
2		ralrimi.2	. . 3 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	alrimi 1811	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2720	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
5	3, 4	sylibr 212	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   A.wal 1367   F/wnf 1589   e. wcel 1756   A.wral 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2720

This theorem is referenced by:  ralrimiv  2798  reximdai  2824  r19.12  2830  rexlimd  2838  rexlimd2  2839  r19.29af2  2860  r19.37  2869  ralcom2  2885  2rmorex  3163  iineq2d  4191  disjxiun  4289  mpteq2da  4377  reusv6OLD  4503  mpteqb  5788  fmptdf  5868  eusvobj2  6084  zfrep6  6545  tfr3  6858  tz7.49  6900  mapxpen  7477  dfac2  8300  hsmexlem4  8598  axcc3  8607  domtriomlem  8611  axdc3lem2  8620  axdc3lem4  8622  axdc4lem  8624  ac6num  8648  dedekind  9533  dedekindle  9534  mreexexd  14586  ptcnplem  19194  xkocnv  19387  cfilucfilOLD  20144  cfilucfil  20145  itg2splitlem  21226  itg2split  21227  itgeq1f  21249  mptelee  23141  funimass4f  25951  fcomptf  25980  offval2f  25983  funcnvmptOLD  25986  funcnvmpt  25987  isarchiofld  26285  esumeq12dvaf  26487  esumel  26501  esumf1o  26504  esumc  26505  esummono  26509  esumlef  26513  esumfsup  26519  esumpinfval  26522  esumpinfsum  26526  measinblem  26634  voliune  26645  volmeas  26647  oms0  26710  dstrvprob  26854  untsucf  27361  trpredmintr  27695  wfrlem4  27727  frrlem4  27771  cover2  28607  upixp  28623  indexdom  28628  filbcmb  28634  sdclem2  28638  eq0rabdioph  29115  eqrabdioph  29116  setindtr  29373  rzalf  29739  fnchoice  29751  refsumcn  29752  rfcnnnub  29758  refsum2cnlem1  29759  climsuse  29781  stoweidlem5  29800  stoweidlem16  29811  stoweidlem18  29813  stoweidlem21  29816  stoweidlem26  29821  stoweidlem27  29822  stoweidlem28  29823  stoweidlem29  29824  stoweidlem31  29826  stoweidlem34  29829  stoweidlem36  29831  stoweidlem41  29836  stoweidlem42  29837  stoweidlem44  29839  stoweidlem45  29840  stoweidlem48  29843  stoweidlem51  29846  stoweidlem55  29850  stoweidlem59  29854  stoweidlem60  29855  stoweidlem62  29857  wallispilem3  29862  stirlinglem5  29873  fsuppmapnn0fiublem  30798  fsuppmapnn0fiub  30799  iunconlem2  31671  bnj1379  31824  bnj1145  31984  bnj1204  32003  bnj1388  32024  bnj1417  32032  bnj1489  32047  bj-rabbida  32421