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

Theorem rabss 3427
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 2722 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq1i 3378 . 2  |-  ( { x  e.  A  |  ph }  C_  B  <->  { x  |  ( x  e.  A  /\  ph ) }  C_  B )
3 abss 3419 . 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 1610 . . 3  |-  ( A. x ( ( x  e.  A  /\  ph )  ->  x  e.  B
)  <->  A. x ( x  e.  A  ->  ( ph  ->  x  e.  B
) ) )
6 df-ral 2718 . . 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 1367    e. wcel 1756   {cab 2427   A.wral 2713   {crab 2717    C_ wss 3326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rab 2722  df-in 3333  df-ss 3340
This theorem is referenced by:  rabssdv  3430  reusv6OLD  4501  fnsuppresOLD  5936  fnsuppres  6714  wemapso2OLD  7764  wemapso2lem  7765  tskwe2  8938  grothac  8995  uzwo3  10946  phibndlem  13843  dfphi2  13847  ramval  14067  gsumvallem1  15498  istopon  18528  ordtrest2lem  18805  filssufilg  19482  cfinufil  19499  blsscls2  20077  nmhmcn  20673  ovolshftlem2  20991  atansssdm  22326  sgmss  22442  sspval  24119  ubthlem2  24270  ordtrest2NEWlem  26350  truae  26657  dvtanlem  28438  nnubfi  28643  prnc  28864  fsuppmapnn0fiub0  30798
  Copyright terms: Public domain W3C validator