Theorem sscon 3599

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 3459	. . . . 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 3447	. . 3 |- ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
5		eldif 3447	. . 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 3471	1 |- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1758   \ cdif 3434   C_ wss 3437

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 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-dif 3440  df-in 3444  df-ss 3451

This theorem is referenced by:  sscond  3602  sorpsscmpl  6482  sbthlem1  7532  sbthlem2  7533  cantnfp1lem1  7998  cantnfp1lem3  8000  cantnfp1lem1OLD  8024  cantnfp1lem3OLD  8026  isf34lem7  8660  isf34lem6  8661  setsres  14321  mplsubglem  17635  mplsubglemOLD  17637  cctop  18743  clsval2  18787  ntrss  18792  hauscmplem  19142  ptbasin  19283  cfinfil  19599  csdfil  19600  uniioombllem5  21201  kur14lem6  27244  dvasin  28629  bj-2upln1upl  32850