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

Theorem ralim 2769
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 2702 . . 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 1570 . . 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 2702 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
6 df-ral 2702 . 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 1549    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ral2imi  2774  r19.30  2845  trint  4309  mpteqb  5811  tfrlem1  6628  tz7.49  6694  abianfp  6708  mptelixpg  7091  resixpfo  7092  bnd  7808  kmlem12  8033  lbzbi  10556  r19.29uz  12146  caubnd  12154  alzdvds  12891  ptclsg  17639  isucn2  18301  dfon2lem8  25409  dford3lem2  27089  usgreghash2spot  28395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ral 2702
  Copyright terms: Public domain W3C validator