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

Theorem ralim 2720
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 2654 . . 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 1567 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  -> 
( A. x ( x  e.  A  ->  ph )  ->  A. x
( x  e.  A  ->  ps ) ) )
41, 3sylbi 188 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x ( x  e.  A  ->  ph )  ->  A. x
( x  e.  A  ->  ps ) ) )
5 df-ral 2654 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
6 df-ral 2654 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
74, 5, 63imtr4g 262 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 1546    e. wcel 1717   A.wral 2649
This theorem is referenced by:  ral2imi  2725  r19.30  2796  trint  4258  mpteqb  5758  tfrlem1  6572  tz7.49  6638  abianfp  6652  mptelixpg  7035  resixpfo  7036  bnd  7749  kmlem12  7974  lbzbi  10496  r19.29uz  12081  caubnd  12089  alzdvds  12826  ptclsg  17568  isucn2  18230  dfon2lem8  25170  dford3lem2  26789
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ral 2654
  Copyright terms: Public domain W3C validator