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

Theorem rabss 3516
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 2763 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq1i 3466 . 2  |-  ( { x  e.  A  |  ph }  C_  B  <->  { x  |  ( x  e.  A  /\  ph ) }  C_  B )
3 abss 3508 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  C_  B  <->  A. x
( ( x  e.  A  /\  ph )  ->  x  e.  B ) )
4 impexp 444 . . . 4  |-  ( ( ( x  e.  A  /\  ph )  ->  x  e.  B )  <->  ( x  e.  A  ->  ( ph  ->  x  e.  B ) ) )
54albii 1661 . . 3  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
6 df-ral 2759 . . 3  |-  ( A. x  e.  A  ( ph  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
75, 6bitr4i 252 . 2  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x  e.  A  ( ph  ->  x  e.  B ) )
82, 3, 73bitri 271 1  |-  ( { x  e.  A  |  ph }  C_  B  <->  A. x  e.  A  ( ph  ->  x  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367   A.wal 1403    e. wcel 1842   {cab 2387   A.wral 2754   {crab 2758    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rab 2763  df-in 3421  df-ss 3428
This theorem is referenced by:  rabssdv  3519  fnsuppresOLD  6113  fnsuppres  6930  wemapso2OLD  8011  wemapso2lem  8012  tskwe2  9181  grothac  9238  uzwo3  11222  fsuppmapnn0fiub0  12143  phibndlem  14509  dfphi2  14513  ramval  14735  mgmidsssn0  16220  istopon  19718  ordtrest2lem  19997  filssufilg  20704  cfinufil  20721  blsscls2  21299  nmhmcn  21895  ovolshftlem2  22213  atansssdm  23589  sgmss  23761  sspval  26050  ubthlem2  26201  ordtrest2NEWlem  28357  truae  28692  dvtanlemOLD  31437  nnubfi  31525  prnc  31746  itgperiod  37148  fourierdlem81  37338  usgresvm1  38072  usgresvm1ALT  38076
  Copyright terms: Public domain W3C validator