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

Theorem ralim 2699
Description: Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
Assertion
Ref Expression
ralim  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x  e.  A  ph  ->  A. x  e.  A  ps )
)

Proof of Theorem ralim
StepHypRef Expression
1 df-ral 2633 . . 3  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
2 ax-2 6 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  ->  ( (
x  e.  A  ->  ph )  ->  ( x  e.  A  ->  ps ) ) )
32al2imi 1566 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  -> 
( A. x ( x  e.  A  ->  ph )  ->  A. x
( x  e.  A  ->  ps ) ) )
41, 3sylbi 187 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x ( x  e.  A  ->  ph )  ->  A. x
( x  e.  A  ->  ps ) ) )
5 df-ral 2633 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
6 df-ral 2633 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
74, 5, 63imtr4g 261 1  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x  e.  A  ph  ->  A. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1545    e. wcel 1715   A.wral 2628
This theorem is referenced by:  ral2imi  2704  r19.30  2770  trint  4230  mpteqb  5721  tfrlem1  6533  tz7.49  6599  abianfp  6613  mptelixpg  6996  resixpfo  6997  bnd  7709  kmlem12  7934  lbzbi  10457  r19.29uz  12041  caubnd  12049  alzdvds  12786  ptclsg  17526  dfon2lem8  24972  dford3lem2  26711  stoweid  27403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562
This theorem depends on definitions:  df-bi 177  df-ral 2633
  Copyright terms: Public domain W3C validator