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

Step	Hyp	Ref	Expression
1		pm3.45 834	. . . 4 |- ( ( x e. A -> x e. B ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
2	1	alimi 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 ) ) )
5	2, 3, 4	3imtr4i 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 ) }
8	5, 6, 7	3sstr4g 3530	1 |- ( A C_ B -> { x e. A | ph } C_ { x e. B | ph } )

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