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

Theorem rexlimd 2819
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 2779 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2813 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 189 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1553    e. wcel 1725   A.wral 2697   E.wrex 2698
This theorem is referenced by:  rexlimdv  2821  reusv2lem2  4717  reusv6OLD  4726  ralxfrALT  4734  peano5  4860  fvmptt  5812  ffnfv  5886  tz7.49  6694  nneneq  7282  ac6sfi  7343  ixpiunwdom  7551  r1val1  7704  rankuni2b  7771  infpssrlem4  8178  zorn2lem4  8371  zorn2lem5  8372  konigthlem  8435  tskuni  8650  gruiin  8677  lbzbi  10556  iunconlem  17482  ptbasfi  17605  alexsubALTlem3  18072  ovoliunnul  19395  iunmbl2  19443  atom1d  23848  elabreximd  23983  iundisjf  24021  esumc  24438  mptelee  25826  indexa  26426  sdclem2  26437  refsumcn  27668  fmul01lt1  27683  stoweidlem27  27743  stoweidlem29  27745  stoweidlem31  27747  stoweidlem35  27751  stoweidlem59  27775  stirlinglem13  27802  ffnafv  28002  glbconxN  30112  cdleme26ee  31094  cdleme32d  31178  cdleme32f  31180  cdlemk38  31649  cdlemk19x  31677  cdlemk11t  31680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator