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

Theorem reximdai 2652
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 2625 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexim 2648 . 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 1685   A.wral 2544   E.wrex 2545
This theorem is referenced by:  reximdvai  2654  tz7.49  6453  hsmexlem2  8049  indexdom  25824  filbcmb  25843  infrglb  27133  climinf  27143  stoweidlem29  27189  stoweidlem31  27191  stoweidlem34  27194  stoweidlem35  27195  2reurex  27350  cdlemefr29exN  29870
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 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator