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

Theorem ralim 2616
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 2550 . . 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 1550 . . 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 2550 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
6 df-ral 2550 . 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 1529    e. wcel 1686   A.wral 2545
This theorem is referenced by:  ral2imi  2621  r19.30  2687  trint  4130  mpteqb  5616  tfrlem1  6393  tz7.49  6459  abianfp  6473  mptelixpg  6855  resixpfo  6856  bnd  7564  kmlem12  7789  lbzbi  10308  r19.29uz  11836  caubnd  11844  alzdvds  12580  ptclsg  17311  dfon2lem8  24148  dford3lem2  27131  stoweid  27823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546
This theorem depends on definitions:  df-bi 177  df-ral 2550
  Copyright terms: Public domain W3C validator