Theorem ssdif 3639

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 3498	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 564	. . 3 |- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif 3486	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3486	. . 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 3510	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1767   \ cdif 3473   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490

This theorem is referenced by:  ssdifd  3640  php  7698  pssnn  7735  mapfienOLD  8134  fin1a2lem13  8788  axcclem  8833  isercolllem3  13448  mvdco  16266  dprdres  16865  dpjidcl  16897  dpjidclOLD  16904  ablfac1eulem  16913  lspsnat  17574  lbsextlem2  17588  lbsextlem3  17589  mplmonmul  17897  cnsubdrglem  18237  clscon  19697  2ndcdisj2  19724  kqdisj  19968  nulmbl2  21682  i1f1  21832  itg11  21833  itg1climres  21856  limcresi  22024  dvreslem  22048  dvres2lem  22049  dvaddbr  22076  dvmulbr  22077  lhop  22152  elqaa  22452  difres  27130  imadifxp  27131  xrge00  27336  eulerpartlemmf  27954  eulerpartlemgf  27958  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  cnambfre  29640  divrngidl  30028  cntzsdrg  30756  fourierdlem62  31469  bj-2upln1upl  33663