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

Theorem rexlimd 2937
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 2818 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
4 rexlimd.2 . . 3  |-  F/ x ch
54r19.23 2931 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  <->  ( E. x  e.  A  ps  ->  ch ) )
63, 5sylib 196 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1590    e. wcel 1758   A.wral 2795   E.wrex 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2800  df-rex 2801
This theorem is referenced by:  rexlimdv  2939  reusv2lem2  4595  reusv6OLD  4604  ralxfrALT  4612  fvmptt  5891  ffnfv  5971  peano5  6602  tz7.49  7003  nneneq  7597  ac6sfi  7660  ixpiunwdom  7910  r1val1  8097  rankuni2b  8164  infpssrlem4  8579  zorn2lem4  8772  zorn2lem5  8773  konigthlem  8836  tskuni  9054  gruiin  9081  lbzbi  11047  iunconlem  19156  ptbasfi  19279  alexsubALTlem3  19746  ovoliunnul  21115  iunmbl2  21164  mptelee  23286  atom1d  25902  elabreximd  26036  iundisjf  26075  esumc  26643  heicant  28567  indexa  28768  sdclem2  28779  refsumcn  29893  fmul01lt1  29908  stoweidlem29  29965  stoweidlem31  29967  stoweidlem59  29995  stirlinglem13  30022  ffnafv  30218  glbconxN  33331  cdleme26ee  34313  cdleme32d  34397  cdleme32f  34399  cdlemk38  34868  cdlemk19x  34896  cdlemk11t  34899
  Copyright terms: Public domain W3C validator