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

Theorem rexlimd 2677
Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Hypotheses
Ref Expression
rexlimd.1  |-  F/ x ph
rexlimd.2  |-  F/ x ch
rexlimd.3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimd  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )

Proof of Theorem rexlimd
StepHypRef Expression
1 rexlimd.1 . . 3  |-  F/ x ph
2 rexlimd.3 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2ralrimi 2637 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2671 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 188 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1534    e. wcel 1696   A.wral 2556   E.wrex 2557
This theorem is referenced by:  rexlimdv  2679  reusv2lem2  4552  reusv6OLD  4561  ralxfrALT  4569  peano5  4695  fvmptt  5631  ffnfv  5701  tz7.49  6473  nneneq  7060  ac6sfi  7117  ixpiunwdom  7321  r1val1  7474  rankuni2b  7541  infpssrlem4  7948  zorn2lem4  8142  zorn2lem5  8143  konigthlem  8206  tskuni  8421  gruiin  8448  lbzbi  10322  iunconlem  17169  ptbasfi  17292  alexsubALTlem3  17759  ovoliunnul  18882  iunmbl2  18930  atom1d  22949  elabreximd  23055  iundisjf  23380  esumc  23445  mptelee  24595  indexa  26515  sdclem2  26555  refsumcn  27804  fmul01lt1  27819  climsuse  27837  stoweidlem27  27879  stoweidlem29  27881  stoweidlem31  27883  stoweidlem35  27887  stoweidlem59  27911  stirlinglem13  27938  ffnafv  28139  glbconxN  30189  cdleme26ee  31171  cdleme32d  31255  cdleme32f  31257  cdlemk38  31726
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-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator