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

Theorem rexlimd 2635
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 2595 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2629 . 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 2516   E.wrex 2517
This theorem is referenced by:  rexlimdv  2637  reusv2lem2  4473  reusv6OLD  4482  ralxfrALT  4490  peano5  4616  fvmptt  5514  ffnfv  5584  tz7.49  6390  nneneq  6977  ac6sfi  7034  ixpiunwdom  7238  r1val1  7391  rankuni2b  7458  infpssrlem4  7865  zorn2lem4  8059  zorn2lem5  8060  konigthlem  8123  tskuni  8338  gruiin  8365  lbzbi  10238  iunconlem  17080  ptbasfi  17203  alexsubALTlem3  17670  ovoliunnul  18793  iunmbl2  18841  atom1d  22858  elabreximd  22965  mptelee  23863  indexa  25744  sdclem2  25784  refsumcn  27034  fmul01lt1  27049  stoweidlem27  27076  stoweidlem29  27078  stoweidlem31  27080  stoweidlem35  27084  stoweidlem59  27108  glbconxN  28697  cdleme26ee  29679  cdleme32d  29763  cdleme32f  29765  cdlemk38  30234
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 2520  df-rex 2521
  Copyright terms: Public domain W3C validator