Theorem rabss2 3536

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 830	. . . 4 |- ( ( x e. A -> x e. B ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
2	1	alimi 1605	. . 3 |- ( A. x ( x e. A -> x e. B ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3		dfss2 3446	. . 3 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		ss2ab 3521	. . 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 2804	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
7		df-rab 2804	. 2 |- { x e. B | ph } = { x | ( x e. B /\ ph ) }
8	5, 6, 7	3sstr4g 3498	1 |- ( A C_ B -> { x e. A | ph } C_ { x e. B | ph } )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1368   e. wcel 1758   {cab 2436   {crab 2799   C_ wss 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-in 3436  df-ss 3443

This theorem is referenced by:  sess2  4790  suppfnss  6817  hashbcss  14176  dprdss  16640  minveclem4  21044  prmdvdsfi  22571  mumul  22645  sqff1o  22646  rpvmasumlem  22862  shatomistici  25910  xpinpreima2  26475  ballotth  27057  rmxyelqirr  29392  idomodle  29702  clwwlknfi  30618  disjxwwlkn  30705  bj-unrab  32732  lssats  32966  lpssat  32967  lssatle  32969  lssat  32970  atlatmstc  33273  dochspss  35332