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

Theorem rexlimd 2665
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 2625 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2659 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 190 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   F/wnf 1536    e. wcel 1688   A.wral 2544   E.wrex 2545
This theorem is referenced by:  rexlimdv  2667  reusv2lem2  4535  reusv6OLD  4544  ralxfrALT  4552  peano5  4678  fvmptt  5576  ffnfv  5646  tz7.49  6452  nneneq  7039  ac6sfi  7096  ixpiunwdom  7300  r1val1  7453  rankuni2b  7520  infpssrlem4  7927  zorn2lem4  8121  zorn2lem5  8122  konigthlem  8185  tskuni  8400  gruiin  8427  lbzbi  10301  iunconlem  17147  ptbasfi  17270  alexsubALTlem3  17737  ovoliunnul  18860  iunmbl2  18908  atom1d  22925  elabreximd  23032  mptelee  23930  indexa  25811  sdclem2  25851  refsumcn  27100  fmul01lt1  27115  climsuse  27133  stoweidlem27  27175  stoweidlem29  27177  stoweidlem31  27179  stoweidlem35  27183  stoweidlem59  27207  stirlinglem13  27234  ffnafv  27410  glbconxN  28834  cdleme26ee  29816  cdleme32d  29900  cdleme32f  29902  cdlemk38  30371
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-nf 1537  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator