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

Theorem rexlimd 2791
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 2751 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2785 . 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 1721   A.wral 2670   E.wrex 2671
This theorem is referenced by:  rexlimdv  2793  reusv2lem2  4688  reusv6OLD  4697  ralxfrALT  4705  peano5  4831  fvmptt  5783  ffnfv  5857  tz7.49  6665  nneneq  7253  ac6sfi  7314  ixpiunwdom  7519  r1val1  7672  rankuni2b  7739  infpssrlem4  8146  zorn2lem4  8339  zorn2lem5  8340  konigthlem  8403  tskuni  8618  gruiin  8645  lbzbi  10524  iunconlem  17447  ptbasfi  17570  alexsubALTlem3  18037  ovoliunnul  19360  iunmbl2  19408  atom1d  23813  elabreximd  23948  iundisjf  23986  esumc  24403  mptelee  25742  indexa  26329  sdclem2  26340  refsumcn  27572  fmul01lt1  27587  stoweidlem27  27647  stoweidlem29  27649  stoweidlem31  27651  stoweidlem35  27655  stoweidlem59  27679  stirlinglem13  27706  ffnafv  27906  glbconxN  29864  cdleme26ee  30846  cdleme32d  30930  cdleme32f  30932  cdlemk38  31401  cdlemk19x  31429  cdlemk11t  31432
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 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675  df-rex 2676
  Copyright terms: Public domain W3C validator