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

Theorem reximdai 2626
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 2599 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexim 2622 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  -> 
( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
53, 4syl 17 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   F/wnf 1539    e. wcel 1621   A.wral 2518   E.wrex 2519
This theorem is referenced by:  reximdvai  2628  tz7.49  6425  hsmexlem2  8021  indexdom  25781  filbcmb  25800  infrglb  27091  climinf  27101  stoweidlem29  27147  stoweidlem31  27149  stoweidlem34  27152  stoweidlem35  27153  2reurex  27308  cdlemefr29exN  29841
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator