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

Theorem ssrab 3264
Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006.)
Assertion
Ref Expression
ssrab  |-  ( B 
C_  { x  e.  A  |  ph }  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem ssrab
StepHypRef Expression
1 df-rab 2565 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq2i 3216 . 2  |-  ( B 
C_  { x  e.  A  |  ph }  <->  B 
C_  { x  |  ( x  e.  A  /\  ph ) } )
3 ssab 3256 . 2  |-  ( B 
C_  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  B  ->  ( x  e.  A  /\  ph ) ) )
4 dfss3 3183 . . . 4  |-  ( B 
C_  A  <->  A. x  e.  B  x  e.  A )
54anbi1i 676 . . 3  |-  ( ( B  C_  A  /\  A. x  e.  B  ph ) 
<->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
6 r19.26 2688 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
7 df-ral 2561 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  A. x ( x  e.  B  ->  (
x  e.  A  /\  ph ) ) )
85, 6, 73bitr2ri 265 . 2  |-  ( A. x ( x  e.  B  ->  ( x  e.  A  /\  ph )
)  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
92, 3, 83bitri 262 1  |-  ( B 
C_  { x  e.  A  |  ph }  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    e. wcel 1696   {cab 2282   A.wral 2556   {crab 2560    C_ wss 3165
This theorem is referenced by:  ssrabdv  3265  omssnlim  4686  ordtypelem2  7250  ordtypelem10  7258  card2inf  7285  r0weon  7656  ramtlecl  13063  sscntz  14818  ppttop  16760  epttop  16762  cmpcov2  17133  tgcmp  17144  xkoinjcn  17397  fbssfi  17548  filssufilg  17622  uffixfr  17634  tmdgsum2  17795  symgtgp  17800  ghmcnp  17813  blcls  18068  clsocv  18693  lhop1lem  19376  ressatans  20246  imambfm  23582  conpcon  23781  cvmlift2lem11  23859  cvmlift2lem12  23860  axcontlem3  24666  axcontlem4  24667  hbtlem6  27436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator