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

Theorem ssrab 3442
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 2736 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq2i 3393 . 2  |-  ( B 
C_  { x  e.  A  |  ph }  <->  B 
C_  { x  |  ( x  e.  A  /\  ph ) } )
3 ssab 3434 . 2  |-  ( B 
C_  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  B  ->  ( x  e.  A  /\  ph ) ) )
4 dfss3 3358 . . . 4  |-  ( B 
C_  A  <->  A. x  e.  B  x  e.  A )
54anbi1i 695 . . 3  |-  ( ( B  C_  A  /\  A. x  e.  B  ph ) 
<->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
6 r19.26 2861 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
7 df-ral 2732 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  A. x ( x  e.  B  ->  (
x  e.  A  /\  ph ) ) )
85, 6, 73bitr2ri 274 . 2  |-  ( A. x ( x  e.  B  ->  ( x  e.  A  /\  ph )
)  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
92, 3, 83bitri 271 1  |-  ( B 
C_  { x  e.  A  |  ph }  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    e. wcel 1756   {cab 2429   A.wral 2727   {crab 2731    C_ wss 3340
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 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2732  df-rab 2736  df-in 3347  df-ss 3354
This theorem is referenced by:  ssrabdv  3443  omssnlim  6502  ordtypelem2  7745  ordtypelem10  7753  card2inf  7782  r0weon  8191  ramtlecl  14073  sscntz  15856  ppttop  18623  epttop  18625  cmpcov2  19005  tgcmp  19016  xkoinjcn  19272  fbssfi  19422  filssufilg  19496  uffixfr  19508  tmdgsum2  19679  symgtgp  19684  ghmcnp  19697  blcls  20093  clsocv  20774  lhop1lem  21497  ressatans  22341  axcontlem3  23224  axcontlem4  23225  imambfm  26689  conpcon  27136  cvmlift2lem11  27214  cvmlift2lem12  27215  hbtlem6  29497  bj-rabtr  32444
  Copyright terms: Public domain W3C validator