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

Theorem rexlimd 2763
Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Hypotheses
Ref Expression
rexlimd.1  |-  F/ x ph
rexlimd.2  |-  F/ x ch
rexlimd.3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimd  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )

Proof of Theorem rexlimd
StepHypRef Expression
1 rexlimd.1 . . 3  |-  F/ x ph
2 rexlimd.3 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
31, 2ralrimi 2723 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2757 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 189 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1550    e. wcel 1717   A.wral 2642   E.wrex 2643
This theorem is referenced by:  rexlimdv  2765  reusv2lem2  4658  reusv6OLD  4667  ralxfrALT  4675  peano5  4801  fvmptt  5752  ffnfv  5826  tz7.49  6631  nneneq  7219  ac6sfi  7280  ixpiunwdom  7485  r1val1  7638  rankuni2b  7705  infpssrlem4  8112  zorn2lem4  8305  zorn2lem5  8306  konigthlem  8369  tskuni  8584  gruiin  8611  lbzbi  10489  iunconlem  17404  ptbasfi  17527  alexsubALTlem3  17994  ovoliunnul  19263  iunmbl2  19311  atom1d  23697  elabreximd  23828  iundisjf  23865  esumc  24235  mptelee  25541  indexa  26119  sdclem2  26130  refsumcn  27362  fmul01lt1  27377  stoweidlem27  27437  stoweidlem29  27439  stoweidlem31  27441  stoweidlem35  27445  stoweidlem59  27469  stirlinglem13  27496  ffnafv  27697  glbconxN  29543  cdleme26ee  30525  cdleme32d  30609  cdleme32f  30611  cdlemk38  31080  cdlemk19x  31108  cdlemk11t  31111
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2647  df-rex 2648
  Copyright terms: Public domain W3C validator