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

Theorem reximdai 2651
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
Hypotheses
Ref Expression
reximdai.1  |-  F/ x ph
reximdai.2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
reximdai  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)

Proof of Theorem reximdai
StepHypRef Expression
1 reximdai.1 . . 3  |-  F/ x ph
2 reximdai.2 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2ralrimi 2624 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexim 2647 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  -> 
( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
53, 4syl 15 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1531    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  reximdvai  2653  tz7.49  6457  hsmexlem2  8053  indexdom  26413  filbcmb  26432  infrglb  27722  climinf  27732  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  2reurex  27959  cdlemefr29exN  30591
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator