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

Theorem ss2rab 3262
Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
Assertion
Ref Expression
ss2rab  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<-> 
A. x  e.  A  ( ph  ->  ps )
)

Proof of Theorem ss2rab
StepHypRef Expression
1 df-rab 2565 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2565 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2sseq12i 3217 . 2  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<->  { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  A  /\  ps ) } )
4 ss2ab 3254 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  A  /\  ps ) } 
<-> 
A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
) )
5 df-ral 2561 . . 3  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 imdistan 670 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
) )
76albii 1556 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps ) ) )
85, 7bitr2i 241 . 2  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
)  <->  A. x  e.  A  ( ph  ->  ps )
)
93, 4, 83bitri 262 1  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<-> 
A. x  e.  A  ( ph  ->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    e. wcel 1696   {cab 2282   A.wral 2556   {crab 2560    C_ wss 3165
This theorem is referenced by:  ss2rabdv  3267  ss2rabi  3268  scottex  7571  ondomon  8201  eltsms  17831  xrlimcnp  20279  occon  21882  spanss  21943  chpssati  22959  rmxyelqirr  27098  itgoss  27471  lpssat  29825  lssatle  29827  lssat  29828  atlatle  30132  pmaple  30572  diaord  31859  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator