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

Theorem ss2rab 3528
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 2804 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2804 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2sseq12i 3482 . 2  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<->  { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  A  /\  ps ) } )
4 ss2ab 3520 . 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 2800 . . 3  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 imdistan 689 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
) )
76albii 1611 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps ) ) )
85, 7bitr2i 250 . 2  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
)  <->  A. x  e.  A  ( ph  ->  ps )
)
93, 4, 83bitri 271 1  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<-> 
A. x  e.  A  ( ph  ->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1368    e. wcel 1758   {cab 2436   A.wral 2795   {crab 2799    C_ wss 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rab 2804  df-in 3435  df-ss 3442
This theorem is referenced by:  ss2rabdv  3533  ss2rabi  3534  scottex  8195  ondomon  8830  eltsms  19821  xrlimcnp  22480  occon  24827  spanss  24888  chpssati  25904  rmxyelqirr  29391  itgoss  29660  wwlknfi  30510  disjxwwlkn  30704  lpssat  32966  lssatle  32968  lssat  32969  atlatle  33273  pmaple  33713  diaord  35000  mapdordlem2  35590
  Copyright terms: Public domain W3C validator