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

Theorem rabss 3570
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 2816 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq1i 3521 . 2  |-  ( { x  e.  A  |  ph }  C_  B  <->  { x  |  ( x  e.  A  /\  ph ) }  C_  B )
3 abss 3562 . 2  |-  ( { x  |  ( x  e.  A  /\  ph ) }  C_  B  <->  A. x
( ( x  e.  A  /\  ph )  ->  x  e.  B ) )
4 impexp 446 . . . 4  |-  ( ( ( x  e.  A  /\  ph )  ->  x  e.  B )  <->  ( x  e.  A  ->  ( ph  ->  x  e.  B ) ) )
54albii 1615 . . 3  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
6 df-ral 2812 . . 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 369   A.wal 1372    e. wcel 1762   {cab 2445   A.wral 2807   {crab 2811    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rab 2816  df-in 3476  df-ss 3483
This theorem is referenced by:  rabssdv  3573  reusv6OLD  4651  fnsuppresOLD  6112  fnsuppres  6917  wemapso2OLD  7966  wemapso2lem  7967  tskwe2  9140  grothac  9197  uzwo3  11166  fsuppmapnn0fiub0  12055  phibndlem  14148  dfphi2  14152  ramval  14374  gsumvallem1  15806  istopon  19186  ordtrest2lem  19463  filssufilg  20140  cfinufil  20157  blsscls2  20735  nmhmcn  21331  ovolshftlem2  21649  atansssdm  22985  sgmss  23101  sspval  25298  ubthlem2  25449  ordtrest2NEWlem  27526  truae  27841  dvtanlem  29628  nnubfi  29833  prnc  30054  itgperiod  31254  fourierdlem81  31443  usgresvm1  31837
  Copyright terms: Public domain W3C validator