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

Theorem reximdai 2901
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 2832 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexim 2897 . 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 setvar class
Syntax hints:    -> wi 4   F/wnf 1663    e. wcel 1870   A.wral 2782   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2787  df-rex 2788
This theorem is referenced by:  reximdvaiOLD  2905  tz7.49  7170  hsmexlem2  8855  acunirnmpt2  28102  acunirnmpt2f  28103  locfinreflem  28506  cmpcref  28516  indexdom  31764  filbcmb  31770  cdlemefr29exN  33677  disjrnmpt2  37085  fompt  37089  disjinfi  37090  supxrge  37169  suplesup  37170  infrglbOLD  37240  limsupre  37292  limsupreOLD  37293  stoweidlem31  37460  stoweidlem34  37463  fourierdlem73  37610  sge0pnffigt  37771  sge0ltfirp  37775  iundjiun  37806  2reurex  37992
  Copyright terms: Public domain W3C validator