Theorem ralrimi 2789

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 1812	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2712	. 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 1362   F/wnf 1594   e. wcel 1757   A.wral 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595  df-ral 2712

This theorem is referenced by:  ralrimiv  2790  reximdai  2816  r19.12  2822  rexlimd  2830  rexlimd2  2831  r19.29af2  2852  r19.37  2861  ralcom2  2877  2rmorex  3154  iineq2d  4181  disjxiun  4279  mpteq2da  4367  reusv6OLD  4493  mpteqb  5778  eusvobj2  6074  zfrep6  6536  tfr3  6846  tz7.49  6888  mapxpen  7467  dfac2  8290  hsmexlem4  8588  axcc3  8597  domtriomlem  8601  axdc3lem2  8610  axdc3lem4  8612  axdc4lem  8614  ac6num  8638  dedekind  9523  dedekindle  9524  mreexexd  14571  ptcnplem  19038  xkocnv  19231  cfilucfilOLD  19988  cfilucfil  19989  itg2splitlem  21070  itg2split  21071  itgeq1f  21093  mptelee  22966  funimass4f  25777  fcomptf  25806  offval2f  25809  funcnvmptOLD  25812  funcnvmpt  25813  isarchiofld  26140  esumeq12dvaf  26343  esumel  26357  esumf1o  26360  esumc  26361  esummono  26365  esumlef  26369  esumfsup  26375  esumpinfval  26378  esumpinfsum  26382  measinblem  26490  voliune  26501  volmeas  26503  dstrvprob  26704  untsucf  27210  trpredmintr  27544  wfrlem4  27576  frrlem4  27620  cover2  28453  upixp  28469  indexdom  28474  filbcmb  28480  sdclem2  28484  eq0rabdioph  28962  eqrabdioph  28963  setindtr  29220  rzalf  29586  fnchoice  29598  refsumcn  29599  rfcnnnub  29605  refsum2cnlem1  29606  fmptdf  29616  climsuse  29629  stoweidlem5  29648  stoweidlem16  29659  stoweidlem18  29661  stoweidlem21  29664  stoweidlem26  29669  stoweidlem27  29670  stoweidlem28  29671  stoweidlem29  29672  stoweidlem31  29674  stoweidlem34  29677  stoweidlem36  29679  stoweidlem41  29684  stoweidlem42  29685  stoweidlem44  29687  stoweidlem45  29688  stoweidlem48  29691  stoweidlem51  29694  stoweidlem52  29695  stoweidlem55  29698  stoweidlem59  29702  stoweidlem60  29703  stoweidlem62  29705  wallispilem3  29710  stirlinglem5  29721  iunconlem2  31413  bnj1379  31566  bnj1145  31726  bnj1204  31745  bnj1388  31766  bnj1417  31774  bnj1489  31789  bj-rabbida  32048