Theorem ssdif 3577

Description: Difference law for subsets. (Contributed by NM, 28-May-1998.)

Assertion

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

Proof of Theorem ssdif

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3435	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 562	. . 3 |- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif 3423	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3423	. . 3 |- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
5	2, 3, 4	3imtr4g 270	. 2 |- ( A C_ B -> ( x e. ( A \ C ) -> x e. ( B \ C ) ) )
6	5	ssrdv 3447	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   e. wcel 1842   \ cdif 3410   C_ wss 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-dif 3416  df-in 3420  df-ss 3427

This theorem is referenced by:  ssdifd  3578  php  7659  pssnn  7693  mapfienOLD  8090  fin1a2lem13  8744  axcclem  8789  isercolllem3  13545  mvdco  16686  dprdres  17287  dpjidcl  17319  dpjidclOLD  17326  ablfac1eulem  17335  lspsnat  18003  lbsextlem2  18017  lbsextlem3  18018  mplmonmul  18338  cnsubdrglem  18681  clscon  20115  2ndcdisj2  20142  kqdisj  20417  nulmbl2  22131  i1f1  22281  itg11  22282  itg1climres  22305  limcresi  22473  dvreslem  22497  dvres2lem  22498  dvaddbr  22525  dvmulbr  22526  lhop  22601  elqaa  22902  difres  27773  imadifxp  27774  xrge00  28006  eulerpartlemmf  28700  eulerpartlemgf  28704  bj-2upln1upl  31135  mblfinlem3  31406  mblfinlem4  31407  ismblfin  31408  cnambfre  31416  divrngidl  31688  cntzsdrg  35496  radcnvrat  36024  fourierdlem62  37301