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

Theorem rabss2 3568
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 834 . . . 4  |-  ( ( x  e.  A  ->  x  e.  B )  ->  ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ph ) ) )
21alimi 1620 . . 3  |-  ( A. x ( x  e.  A  ->  x  e.  B )  ->  A. x
( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ph ) ) )
3 dfss2 3478 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 ss2ab 3553 . . 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 266 . 2  |-  ( A 
C_  B  ->  { x  |  ( x  e.  A  /\  ph ) }  C_  { x  |  ( x  e.  B  /\  ph ) } )
6 df-rab 2802 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
7 df-rab 2802 . 2  |-  { x  e.  B  |  ph }  =  { x  |  ( x  e.  B  /\  ph ) }
85, 6, 73sstr4g 3530 1  |-  ( A 
C_  B  ->  { x  e.  A  |  ph }  C_ 
{ x  e.  B  |  ph } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1381    e. wcel 1804   {cab 2428   {crab 2797    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475
This theorem is referenced by:  sess2  4838  suppfnss  6927  hashbcss  14503  dprdss  17054  minveclem4  21824  prmdvdsfi  23357  mumul  23431  sqff1o  23432  rpvmasumlem  23648  disjxwwlkn  24721  clwwlknfi  24754  shatomistici  27256  rabfodom  27380  xpinpreima2  27866  ballotth  28453  rmxyelqirr  30821  idomodle  31129  bj-unrab  34242  lssats  34477  lpssat  34478  lssatle  34480  lssat  34481  atlatmstc  34784  dochspss  36845
  Copyright terms: Public domain W3C validator