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

Theorem rabss2 3418
Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
rabss2  |-  ( A 
C_  B  ->  { x  e.  A  |  ph }  C_ 
{ x  e.  B  |  ph } )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rabss2
StepHypRef Expression
1 pm3.45 808 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  ->  ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ph ) ) )
21alimi 1568 . . 3  |-  ( A. x ( x  e.  A  ->  x  e.  B )  ->  A. x
( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ph ) ) )
3 dfss2 3329 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 ss2ab 3403 . . 3  |-  ( { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  B  /\  ph ) } 
<-> 
A. x ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ph )
) )
52, 3, 43imtr4i 258 . 2  |-  ( A 
C_  B  ->  { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  B  /\  ph ) } )
6 df-rab 2706 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
7 df-rab 2706 . 2  |-  { x  e.  B  |  ph }  =  { x  |  ( x  e.  B  /\  ph ) }
85, 6, 73sstr4g 3381 1  |-  ( A 
C_  B  ->  { x  e.  A  |  ph }  C_ 
{ x  e.  B  |  ph } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549    e. wcel 1725   {cab 2421   {crab 2701    C_ wss 3312
This theorem is referenced by:  sess2  4543  hashbcss  13364  dprdss  15579  minveclem4  19325  prmdvdsfi  20882  mumul  20956  sqff1o  20957  rpvmasumlem  21173  shatomistici  23856  xpinpreima2  24297  ballotth  24787  rmxyelqirr  26964  idomodle  27480  lssats  29747  lpssat  29748  lssatle  29750  lssat  29751  atlatmstc  30054  dochspss  32113
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator