Theorem rabss2 3497

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

Step	Hyp	Ref	Expression
1		pm3.45 832	. . . 4 |- ( ( x e. A -> x e. B ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
2	1	alimi 1641	. . 3 |- ( A. x ( x e. A -> x e. B ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3		dfss2 3406	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ss2ab 3482	. . 3 |- ( { x | ( x e. A /\ ph ) } C_ { x | ( x e. B /\ ph ) } <-> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
5	2, 3, 4	3imtr4i 266	. 2 |- ( A C_ B -> { x | ( x e. A /\ ph ) } C_ { x | ( x e. B /\ ph ) } )
6		df-rab 2741	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
7		df-rab 2741	. 2 |- { x e. B | ph } = { x | ( x e. B /\ ph ) }
8	5, 6, 7	3sstr4g 3458	1 |- ( A C_ B -> { x e. A | ph } C_ { x e. B | ph } )

Syntax hints:   -> wi 4   /\ wa 367   A.wal 1397   e. wcel 1826   {cab 2367   {crab 2736   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-in 3396  df-ss 3403

This theorem is referenced by:  sess2  4762  suppfnss  6843  hashbcss  14524  dprdss  17189  minveclem4  21932  prmdvdsfi  23498  mumul  23572  sqff1o  23573  rpvmasumlem  23789  disjxwwlkn  24866  clwwlknfi  24899  shatomistici  27396  rabfodom  27522  xpinpreima2  28043  ballotth  28659  rmxyelqirr  31011  idomodle  31321  bj-unrab  34841  lssats  35150  lpssat  35151  lssatle  35153  lssat  35154  atlatmstc  35457  dochspss  37518