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

Theorem rexlimd 2637
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 2597 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2631 . 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  2639  reusv2lem2  4494  reusv6OLD  4503  ralxfrALT  4511  peano5  4637  fvmptt  5535  ffnfv  5605  tz7.49  6411  nneneq  6998  ac6sfi  7055  ixpiunwdom  7259  r1val1  7412  rankuni2b  7479  infpssrlem4  7886  zorn2lem4  8080  zorn2lem5  8081  konigthlem  8144  tskuni  8359  gruiin  8386  lbzbi  10259  iunconlem  17101  ptbasfi  17224  alexsubALTlem3  17691  ovoliunnul  18814  iunmbl2  18862  atom1d  22879  elabreximd  22986  mptelee  23884  indexa  25765  sdclem2  25805  refsumcn  27055  fmul01lt1  27070  stoweidlem27  27097  stoweidlem29  27099  stoweidlem31  27101  stoweidlem35  27105  stoweidlem59  27129  glbconxN  28718  cdleme26ee  29700  cdleme32d  29784  cdleme32f  29786  cdlemk38  30255
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 2521  df-rex 2522
  Copyright terms: Public domain W3C validator