Theorem sscon 3623

Description: Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
sscon	|- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Proof of Theorem sscon

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3483	. . . . 5 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	con3d 133	. . . 4 |- ( A C_ B -> ( -. x e. B -> -. x e. A ) )
3	2	anim2d 565	. . 3 |- ( A C_ B -> ( ( x e. C /\ -. x e. B ) -> ( x e. C /\ -. x e. A ) ) )
4		eldif 3471	. . 3 |- ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
5		eldif 3471	. . 3 |- ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
6	3, 4, 5	3imtr4g 270	. 2 |- ( A C_ B -> ( x e. ( C \ B ) -> x e. ( C \ A ) ) )
7	6	ssrdv 3495	1 |- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1804   \ cdif 3458   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-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-v 3097  df-dif 3464  df-in 3468  df-ss 3475

This theorem is referenced by:  sscond  3626  sorpsscmpl  6576  sbthlem1  7629  sbthlem2  7630  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  isf34lem7  8762  isf34lem6  8763  setsres  14537  mplsubglem  17967  mplsubglemOLD  17969  cctop  19380  clsval2  19424  ntrss  19429  hauscmplem  19779  ptbasin  19951  cfinfil  20267  csdfil  20268  uniioombllem5  21869  kur14lem6  28528  dvasin  30078  fourierdlem62  31840  bj-2upln1upl  34324