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

Theorem ssrab 3564
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 2813 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq2i 3514 . 2  |-  ( B 
C_  { x  e.  A  |  ph }  <->  B 
C_  { x  |  ( x  e.  A  /\  ph ) } )
3 ssab 3556 . 2  |-  ( B 
C_  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  B  ->  ( x  e.  A  /\  ph ) ) )
4 dfss3 3479 . . . 4  |-  ( B 
C_  A  <->  A. x  e.  B  x  e.  A )
54anbi1i 693 . . 3  |-  ( ( B  C_  A  /\  A. x  e.  B  ph ) 
<->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
6 r19.26 2981 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
7 df-ral 2809 . . 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 367   A.wal 1396    e. wcel 1823   {cab 2439   A.wral 2804   {crab 2808    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rab 2813  df-in 3468  df-ss 3475
This theorem is referenced by:  ssrabdv  3565  omssnlim  6687  ordtypelem2  7936  ordtypelem10  7944  card2inf  7973  r0weon  8381  ramtlecl  14602  sscntz  16563  ppttop  19675  epttop  19677  cmpcov2  20057  tgcmp  20068  xkoinjcn  20354  fbssfi  20504  filssufilg  20578  uffixfr  20590  tmdgsum2  20761  symgtgp  20766  ghmcnp  20779  blcls  21175  clsocv  21856  lhop1lem  22580  ressatans  23462  axcontlem3  24471  axcontlem4  24472  imambfm  28470  conpcon  28944  cvmlift2lem11  29022  cvmlift2lem12  29023  hbtlem6  31319  bj-rabtr  34898
  Copyright terms: Public domain W3C validator