Theorem sscon 3485

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 3345	. . . . 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 3333	. . 3 |- ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
5		eldif 3333	. . 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 3357	1 |- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1756   \ cdif 3320   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326  df-in 3330  df-ss 3337

This theorem is referenced by:  sscond  3488  sorpsscmpl  6366  sbthlem1  7413  sbthlem2  7414  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  isf34lem7  8540  isf34lem6  8541  setsres  14194  mplsubglem  17487  mplsubglemOLD  17489  cctop  18585  clsval2  18629  ntrss  18634  hauscmplem  18984  ptbasin  19125  cfinfil  19441  csdfil  19442  uniioombllem5  21042  kur14lem6  27051  dvasin  28433  bj-2upln1upl  32364