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

Theorem rexlimd 2664
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 2624 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2658 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 188 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1531    e. wcel 1684   A.wral 2543   E.wrex 2544
This theorem is referenced by:  rexlimdv  2666  reusv2lem2  4536  reusv6OLD  4545  ralxfrALT  4553  peano5  4679  fvmptt  5615  ffnfv  5685  tz7.49  6457  nneneq  7044  ac6sfi  7101  ixpiunwdom  7305  r1val1  7458  rankuni2b  7525  infpssrlem4  7932  zorn2lem4  8126  zorn2lem5  8127  konigthlem  8190  tskuni  8405  gruiin  8432  lbzbi  10306  iunconlem  17153  ptbasfi  17276  alexsubALTlem3  17743  ovoliunnul  18866  iunmbl2  18914  atom1d  22933  elabreximd  23039  iundisjf  23365  esumc  23430  mptelee  24523  indexa  26412  sdclem2  26452  refsumcn  27701  fmul01lt1  27716  climsuse  27734  stoweidlem27  27776  stoweidlem29  27778  stoweidlem31  27780  stoweidlem35  27784  stoweidlem59  27808  stirlinglem13  27835  ffnafv  28033  glbconxN  29567  cdleme26ee  30549  cdleme32d  30633  cdleme32f  30635  cdlemk38  31104
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 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator