Theorem sscon 3624

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 563	. . 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 367   e. wcel 1823   \ 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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475

This theorem is referenced by:  sscond  3627  sorpsscmpl  6564  sbthlem1  7620  sbthlem2  7621  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  isf34lem7  8750  isf34lem6  8751  setsres  14746  mplsubglem  18288  mplsubglemOLD  18290  cctop  19674  clsval2  19718  ntrss  19723  hauscmplem  20073  ptbasin  20244  cfinfil  20560  csdfil  20561  uniioombllem5  22162  kur14lem6  28919  dvasin  30343  fourierdlem62  32190  bj-2upln1upl  34983