Theorem sscon 3535

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 3394	. . . . 5 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	con3d 140	. . . 4 |- ( A C_ B -> ( -. x e. B -> -. x e. A ) )
3	2	anim2d 573	. . 3 |- ( A C_ B -> ( ( x e. C /\ -. x e. B ) -> ( x e. C /\ -. x e. A ) ) )
4		eldif 3382	. . 3 |- ( x e. ( C \ B ) <-> ( x e. C /\ -. x e. B ) )
5		eldif 3382	. . 3 |- ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
6	3, 4, 5	3imtr4g 278	. 2 |- ( A C_ B -> ( x e. ( C \ B ) -> x e. ( C \ A ) ) )
7	6	ssrdv 3406	1 |- ( A C_ B -> ( C \ B ) C_ ( C \ A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 375   e. wcel 1891   \ cdif 3369   C_ wss 3372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-dif 3375  df-in 3379  df-ss 3386

This theorem is referenced by:  sscond  3538  sorpsscmpl  6570  sbthlem1  7669  sbthlem2  7670  cantnfp1lem1  8170  cantnfp1lem3  8172  isf34lem7  8796  isf34lem6  8797  setsres  15162  mplsubglem  18669  cctop  20032  clsval2  20076  ntrss  20081  hauscmplem  20432  ptbasin  20603  cfinfil  20919  csdfil  20920  uniioombllem5  22557  kur14lem6  29940  bj-2upln1upl  31620  dvasin  32030  fourierdlem62  38089  caragendifcl  38399