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

Theorem ralim 2745
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 2679 . . 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 2679 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
6 df-ral 2679 . 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 1721   A.wral 2674
This theorem is referenced by:  ral2imi  2750  r19.30  2821  trint  4285  mpteqb  5786  tfrlem1  6603  tz7.49  6669  abianfp  6683  mptelixpg  7066  resixpfo  7067  bnd  7780  kmlem12  8005  lbzbi  10528  r19.29uz  12117  caubnd  12125  alzdvds  12862  ptclsg  17608  isucn2  18270  dfon2lem8  25368  dford3lem2  26996  usgreghash2spot  28180
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 2679
  Copyright terms: Public domain W3C validator