Theorem rabss 3679

Description: Restricted class abstraction in a subclass relationship. (Contributed by NM, 16-Aug-2006.)

Assertion

Ref	Expression
rabss	|- ( { x e. A | ph } C_ B <-> A. x e. A ( ph -> x e. B ) )

Distinct variable group:   x, B

Allowed substitution hints:   ph( x)   A( x)

Proof of Theorem rabss

Step	Hyp	Ref	Expression
1		df-rab 2921	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2	1	sseq1i 3629	. 2 |- ( { x e. A | ph } C_ B <-> { x | ( x e. A /\ ph ) } C_ B )
3		abss 3671	. 2 |- ( { x | ( x e. A /\ ph ) } C_ B <-> A. x ( ( x e. A /\ ph ) -> x e. B ) )
4		impexp 462	. . . 4 |- ( ( ( x e. A /\ ph ) -> x e. B ) <-> ( x e. A -> ( ph -> x e. B ) ) )
5	4	albii 1747	. . 3 |- ( A. x ( ( x e. A /\ ph ) -> x e. B ) <-> A. x ( x e. A -> ( ph -> x e. B ) ) )
6		df-ral 2917	. . 3 |- ( A. x e. A ( ph -> x e. B ) <-> A. x ( x e. A -> ( ph -> x e. B ) ) )
7	5, 6	bitr4i 267	. 2 |- ( A. x ( ( x e. A /\ ph ) -> x e. B ) <-> A. x e. A ( ph -> x e. B ) )
8	2, 3, 7	3bitri 286	1 |- ( { x e. A | ph } C_ B <-> A. x e. A ( ph -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   e. wcel 1990   {cab 2608   A.wral 2912   {crab 2916   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-in 3581  df-ss 3588

This theorem is referenced by:  rabssdv  3682  fnsuppres  7322  wemapso2lem  8457  tskwe2  9595  grothac  9652  uzwo3  11783  fsuppmapnn0fiub0  12793  dvdsssfz1  15040  phibndlem  15475  dfphi2  15479  ramval  15712  mgmidsssn0  17269  istopon  20717  ordtrest2lem  21007  filssufilg  21715  cfinufil  21732  blsscls2  22309  nmhmcn  22920  ovolshftlem2  23278  atansssdm  24660  umgrres1lem  26202  upgrres1  26205  sspval  27578  ubthlem2  27727  ordtrest2NEWlem  29968  truae  30306  poimirlem30  33439  nnubfi  33546  prnc  33866  supminfrnmpt  39672  supminfxrrnmpt  39701  itgperiod  40197  fourierdlem81  40404  ovnsupge0  40771  smflimlem2  40980