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

Theorem rabss 3412
Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
rabss  |-  ( { x  e.  A  |  ph }  C_  B  <->  A. x  e.  A  ( ph  ->  x  e.  B ) )
Distinct variable group:    x, B
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rabss
StepHypRef Expression
1 df-rab 2706 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq1i 3364 . 2  |-  ( { x  e.  A  |  ph }  C_  B  <->  { x  |  ( x  e.  A  /\  ph ) }  C_  B )
3 abss 3404 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  C_  B  <->  A. x
( ( x  e.  A  /\  ph )  ->  x  e.  B ) )
4 impexp 434 . . . 4  |-  ( ( ( x  e.  A  /\  ph )  ->  x  e.  B )  <->  ( x  e.  A  ->  ( ph  ->  x  e.  B ) ) )
54albii 1575 . . 3  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
6 df-ral 2702 . . 3  |-  ( A. x  e.  A  ( ph  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
75, 6bitr4i 244 . 2  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x  e.  A  ( ph  ->  x  e.  B ) )
82, 3, 73bitri 263 1  |-  ( { x  e.  A  |  ph }  C_  B  <->  A. x  e.  A  ( ph  ->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    e. wcel 1725   {cab 2421   A.wral 2697   {crab 2701    C_ wss 3312
This theorem is referenced by:  rabssdv  3415  reusv6OLD  4726  fnsuppres  5944  wemapso2  7513  tskwe2  8640  grothac  8697  uzwo3  10561  phibndlem  13151  dfphi2  13155  ramval  13368  gsumvallem1  14763  istopon  16982  ordtrest2lem  17259  filssufilg  17935  cfinufil  17952  blsscls2  18526  nmhmcn  19120  ovolshftlem2  19398  atansssdm  20765  sgmss  20881  sspval  22214  ubthlem2  22365  truae  24586  nnubfi  26445  prnc  26668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rab 2706  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator