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

Theorem ssrab 3422
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 2715 . . 3  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21sseq2i 3374 . 2  |-  ( B 
C_  { x  e.  A  |  ph }  <->  B 
C_  { x  |  ( x  e.  A  /\  ph ) } )
3 ssab 3414 . 2  |-  ( B 
C_  { x  |  ( x  e.  A  /\  ph ) }  <->  A. x
( x  e.  B  ->  ( x  e.  A  /\  ph ) ) )
4 dfss3 3339 . . . 4  |-  ( B 
C_  A  <->  A. x  e.  B  x  e.  A )
54anbi1i 678 . . 3  |-  ( ( B  C_  A  /\  A. x  e.  B  ph ) 
<->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
6 r19.26 2839 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  ( A. x  e.  B  x  e.  A  /\  A. x  e.  B  ph ) )
7 df-ral 2711 . . 3  |-  ( A. x  e.  B  (
x  e.  A  /\  ph )  <->  A. x ( x  e.  B  ->  (
x  e.  A  /\  ph ) ) )
85, 6, 73bitr2ri 267 . 2  |-  ( A. x ( x  e.  B  ->  ( x  e.  A  /\  ph )
)  <->  ( B  C_  A  /\  A. x  e.  B  ph ) )
92, 3, 83bitri 264 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 178    /\ wa 360   A.wal 1550    e. wcel 1726   {cab 2423   A.wral 2706   {crab 2710    C_ wss 3321
This theorem is referenced by:  ssrabdv  3423  omssnlim  4860  ordtypelem2  7489  ordtypelem10  7497  card2inf  7524  r0weon  7895  ramtlecl  13369  sscntz  15126  ppttop  17072  epttop  17074  cmpcov2  17454  tgcmp  17465  xkoinjcn  17720  fbssfi  17870  filssufilg  17944  uffixfr  17956  tmdgsum2  18127  symgtgp  18132  ghmcnp  18145  blcls  18537  clsocv  19205  lhop1lem  19898  ressatans  20775  imambfm  24613  conpcon  24923  cvmlift2lem11  25001  cvmlift2lem12  25002  axcontlem3  25906  axcontlem4  25907  hbtlem6  27311
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rab 2715  df-in 3328  df-ss 3335
  Copyright terms: Public domain W3C validator