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

Theorem reximdai 2856
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 2788 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexim 2852 . 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 1667    e. wcel 1887   A.wral 2737   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742  df-rex 2743
This theorem is referenced by:  reximdvaiOLD  2860  tz7.49  7162  hsmexlem2  8857  acunirnmpt2  28262  acunirnmpt2f  28263  locfinreflem  28667  cmpcref  28677  indexdom  32061  filbcmb  32067  cdlemefr29exN  33969  disjrnmpt2  37463  fompt  37467  disjinfi  37468  supxrge  37561  suplesup  37562  infrglbOLD  37669  limsupre  37721  limsupreOLD  37722  stoweidlem31  37892  stoweidlem34  37895  fourierdlem73  38043  sge0pnffigt  38238  sge0ltfirp  38242  iundjiun  38298  ovnlerp  38384  2reurex  38602
  Copyright terms: Public domain W3C validator