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

Theorem ss2rab 3537
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 2780 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
2 df-rab 2780 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
31, 2sseq12i 3490 . 2  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<->  { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  A  /\  ps ) } )
4 ss2ab 3529 . 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 2776 . . 3  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 imdistan 693 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
) )
76albii 1685 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps ) ) )
85, 7bitr2i 253 . 2  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  A  /\  ps )
)  <->  A. x  e.  A  ( ph  ->  ps )
)
93, 4, 83bitri 274 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 187    /\ wa 370   A.wal 1435    e. wcel 1872   {cab 2407   A.wral 2771   {crab 2775    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rab 2780  df-in 3443  df-ss 3450
This theorem is referenced by:  ss2rabdv  3542  ss2rabi  3543  scottex  8364  ondomon  8995  eltsms  21145  xrlimcnp  23892  wwlknfi  25464  disjxwwlkn  25471  occon  26938  spanss  26999  chpssati  28014  mptexgf  28227  lpssat  32548  lssatle  32550  lssat  32551  atlatle  32855  pmaple  33295  diaord  34584  mapdordlem2  35174  rmxyelqirr  35728  itgoss  35999  ovnsslelem  38286
  Copyright terms: Public domain W3C validator