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

Theorem rexlimd 2626
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 2586 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2620 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 190 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   F/wnf 1539    e. wcel 1621   A.wral 2509   E.wrex 2510
This theorem is referenced by:  rexlimdv  2628  reusv2lem2  4427  reusv6OLD  4436  ralxfrALT  4444  peano5  4570  fvmptt  5467  ffnfv  5537  tz7.49  6343  nneneq  6929  ac6sfi  6986  ixpiunwdom  7189  r1val1  7342  rankuni2b  7409  infpssrlem4  7816  zorn2lem4  8010  zorn2lem5  8011  konigthlem  8070  tskuni  8285  gruiin  8312  lbzbi  10185  iunconlem  16985  ptbasfi  17108  alexsubALTlem3  17575  ovoliunnul  18698  iunmbl2  18746  atom1d  22763  mptelee  23697  indexa  25578  sdclem2  25618  glbconxN  28256  cdleme26ee  29238  cdleme32d  29322  cdleme32f  29324  cdlemk38  29793
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator